Metamath Proof Explorer

Theorem cvllat

Description: An atomic lattice with the covering property is a lattice. (Contributed by NM, 5-Nov-2012)

		Ref	Expression
	Assertion	cvllat	$⊢ K \in CvLat \to K \in Lat$

Step	Hyp	Ref	Expression
1		cvlatl	$⊢ K \in CvLat \to K \in AtLat$
2		atllat	$⊢ K \in AtLat \to K \in Lat$
3	1 2	syl	$⊢ K \in CvLat \to K \in Lat$