Theorem atcvrj2

Description: Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012)

	Ref	Expression
Hypotheses	atcvrj1x.l	|- .<_ = ( le ` K )
	atcvrj1x.j	|- .\/ = ( join ` K )
	atcvrj1x.c	|- C = (
	atcvrj1x.a	|- A = ( Atoms ` K )
Assertion	atcvrj2	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) -> P C ( Q .\/ R ) )

Proof

Step	Hyp	Ref	Expression
1		atcvrj1x.l	|- .<_ = ( le ` K )
2		atcvrj1x.j	|- .\/ = ( join ` K )
3		atcvrj1x.c	|- C = (
4		atcvrj1x.a	|- A = ( Atoms ` K )
5	1 2 3 4	atcvrj2b	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( Q =/= R /\ P .<_ ( Q .\/ R ) ) <-> P C ( Q .\/ R ) ) )
6	5	biimp3a	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ P .<_ ( Q .\/ R ) ) ) -> P C ( Q .\/ R ) )