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	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ ) )

Proof

Step	Hyp	Ref	Expression
1		chsh	⊢ ( 𝐴 ∈ Cℋ → 𝐴 ∈ Sℋ )
2		shle0	⊢ ( 𝐴 ∈ Sℋ → ( 𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ ) )
3	1 2	syl	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ ) )