Theorem atcvr2

Description: An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012)

	Ref	Expression
Hypotheses	atcvr1.j	|- .\/ = ( join ` K )
	atcvr1.c	|- C = (
	atcvr1.a	|- A = ( Atoms ` K )
Assertion	atcvr2	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P =/= Q <-> P C ( Q .\/ P ) ) )

Proof

Step	Hyp	Ref	Expression
1		atcvr1.j	|- .\/ = ( join ` K )
2		atcvr1.c	|- C = (
3		atcvr1.a	|- A = ( Atoms ` K )
4		hlomcmcv	|- ( K e. HL -> ( K e. OML /\ K e. CLat /\ K e. CvLat ) )
5	1 2 3	cvlatcvr2	|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ P e. A /\ Q e. A ) -> ( P =/= Q <-> P C ( Q .\/ P ) ) )
6	4 5	syl3an1	|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P =/= Q <-> P C ( Q .\/ P ) ) )