Theorem cvlatl

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

	Ref	Expression
Assertion	cvlatl	|- ( K e. CvLat -> K e. AtLat )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` K ) = ( Base ` K )
2		eqid	|- ( le ` K ) = ( le ` K )
3		eqid	|- ( join ` K ) = ( join ` K )
4		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
5	1 2 3 4	iscvlat	|- ( K e. CvLat <-> ( K e. AtLat /\ A. p e. ( Atoms ` K ) A. q e. ( Atoms ` K ) A. x e. ( Base ` K ) ( ( -. p ( le ` K ) x /\ p ( le ` K ) ( x ( join ` K ) q ) ) -> q ( le ` K ) ( x ( join ` K ) p ) ) ) )
6	5	simplbi	|- ( K e. CvLat -> K e. AtLat )