Theorem lhpexle

Description: There exists an atom under a co-atom. (Contributed by NM, 26-Apr-2013)

	Ref	Expression
Hypotheses	lhp2a.l	|- .<_ = ( le ` K )
	lhp2a.a	|- A = ( Atoms ` K )
	lhp2a.h	|- H = ( LHyp ` K )
Assertion	lhpexle	|- ( ( K e. HL /\ W e. H ) -> E. p e. A p .<_ W )

Proof

Step	Hyp	Ref	Expression
1		lhp2a.l	|- .<_ = ( le ` K )
2		lhp2a.a	|- A = ( Atoms ` K )
3		lhp2a.h	|- H = ( LHyp ` K )
4		simpl	|- ( ( K e. HL /\ W e. H ) -> K e. HL )
5		eqid	|- ( Base ` K ) = ( Base ` K )
6	5 3	lhpbase	|- ( W e. H -> W e. ( Base ` K ) )
7	6	adantl	|- ( ( K e. HL /\ W e. H ) -> W e. ( Base ` K ) )
8		eqid	|- ( 0. ` K ) = ( 0. ` K )
9	8 3	lhpn0	|- ( ( K e. HL /\ W e. H ) -> W =/= ( 0. ` K ) )
10	5 1 8 2	atle	|- ( ( K e. HL /\ W e. ( Base ` K ) /\ W =/= ( 0. ` K ) ) -> E. p e. A p .<_ W )
11	4 7 9 10	syl3anc	|- ( ( K e. HL /\ W e. H ) -> E. p e. A p .<_ W )