Theorem chm0i

Description: Meet with Hilbert lattice zero. (Contributed by NM, 6-Aug-2004) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ch0le.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	chm0i	$$⊢A\cap 0_{\mathscr{H}}=0_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		inss2	$$⊢A\cap 0_{\mathscr{H}}\subseteq 0_{\mathscr{H}}$$
3	1	ch0lei	$$⊢0_{\mathscr{H}}\subseteq A$$
4		ssid	$$⊢0_{\mathscr{H}}\subseteq 0_{\mathscr{H}}$$
5	3 4	ssini	$$⊢0_{\mathscr{H}}\subseteq A\cap 0_{\mathscr{H}}$$
6	2 5	eqssi	$$⊢A\cap 0_{\mathscr{H}}=0_{\mathscr{H}}$$