Metamath Proof Explorer

Theorem hlomcmat

Description: A Hilbert lattice is orthomodular, complete, and atomic. (Contributed by NM, 5-Nov-2012)

		Ref	Expression
	Assertion	hlomcmat	$⊢ K \in HL \to (K \in OML \land K \in CLat \land K \in AtLat)$

Step	Hyp	Ref	Expression
1		hloml	$⊢ K \in HL \to K \in OML$
2		hlclat	$⊢ K \in HL \to K \in CLat$
3		hlatl	$⊢ K \in HL \to K \in AtLat$
4	1 2 3	3jca	$⊢ K \in HL \to (K \in OML \land K \in CLat \land K \in AtLat)$