Theorem chle0

Description: No Hilbert lattice element is smaller than zero. (Contributed by NM, 14-Aug-2002) (New usage is discouraged.)

	Ref	Expression
Assertion	chle0	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(A\subseteq 0_{\mathscr{H}}\leftrightarrow A=0_{\mathscr{H}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		chsh	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A\in {\mathbf{S}}_{\mathscr{H}}$$
2		shle0	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to \left(A\subseteq 0_{\mathscr{H}}\leftrightarrow A=0_{\mathscr{H}}\right)$$
3	1 2	syl	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(A\subseteq 0_{\mathscr{H}}\leftrightarrow A=0_{\mathscr{H}}\right)$$