Theorem islln2

Description: The predicate "is a lattice line". (Contributed by NM, 23-Jun-2012)

	Ref	Expression
Hypotheses	islln3.b	|- B = ( Base ` K )
	islln3.j	|- .\/ = ( join ` K )
	islln3.a	|- A = ( Atoms ` K )
	islln3.n	|- N = ( LLines ` K )
Assertion	islln2	|- ( K e. HL -> ( X e. N <-> ( X e. B /\ E. p e. A E. q e. A ( p =/= q /\ X = ( p .\/ q ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		islln3.b	|- B = ( Base ` K )
2		islln3.j	|- .\/ = ( join ` K )
3		islln3.a	|- A = ( Atoms ` K )
4		islln3.n	|- N = ( LLines ` K )
5	1 4	llnbase	|- ( X e. N -> X e. B )
6	5	pm4.71ri	|- ( X e. N <-> ( X e. B /\ X e. N ) )
7	1 2 3 4	islln3	|- ( ( K e. HL /\ X e. B ) -> ( X e. N <-> E. p e. A E. q e. A ( p =/= q /\ X = ( p .\/ q ) ) ) )
8	7	pm5.32da	|- ( K e. HL -> ( ( X e. B /\ X e. N ) <-> ( X e. B /\ E. p e. A E. q e. A ( p =/= q /\ X = ( p .\/ q ) ) ) ) )
9	6 8	syl5bb	|- ( K e. HL -> ( X e. N <-> ( X e. B /\ E. p e. A E. q e. A ( p =/= q /\ X = ( p .\/ q ) ) ) ) )