Theorem paddasslem1

Description: Lemma for paddass . (Contributed by NM, 8-Jan-2012)

	Ref	Expression
Hypotheses	paddasslem.l	|- .<_ = ( le ` K )
	paddasslem.j	|- .\/ = ( join ` K )
	paddasslem.a	|- A = ( Atoms ` K )
Assertion	paddasslem1	|- ( ( ( K e. HL /\ ( x e. A /\ r e. A /\ y e. A ) /\ x =/= y ) /\ -. r .<_ ( x .\/ y ) ) -> -. x .<_ ( r .\/ y ) )

Proof

Step	Hyp	Ref	Expression
1		paddasslem.l	|- .<_ = ( le ` K )
2		paddasslem.j	|- .\/ = ( join ` K )
3		paddasslem.a	|- A = ( Atoms ` K )
4	1 2 3	hlatexch2	|- ( ( K e. HL /\ ( x e. A /\ r e. A /\ y e. A ) /\ x =/= y ) -> ( x .<_ ( r .\/ y ) -> r .<_ ( x .\/ y ) ) )
5	4	con3dimp	|- ( ( ( K e. HL /\ ( x e. A /\ r e. A /\ y e. A ) /\ x =/= y ) /\ -. r .<_ ( x .\/ y ) ) -> -. x .<_ ( r .\/ y ) )