Theorem islhp2

Description: The predicate "is a co-atom (lattice hyperplane)". (Contributed by NM, 18-May-2012)

	Ref	Expression
Hypotheses	lhpset.b	|- B = ( Base ` K )
	lhpset.u	|- .1. = ( 1. ` K )
	lhpset.c	|- C = (
	lhpset.h	|- H = ( LHyp ` K )
Assertion	islhp2	|- ( ( K e. A /\ W e. B ) -> ( W e. H <-> W C .1. ) )

Proof

Step	Hyp	Ref	Expression
1		lhpset.b	|- B = ( Base ` K )
2		lhpset.u	|- .1. = ( 1. ` K )
3		lhpset.c	|- C = (
4		lhpset.h	|- H = ( LHyp ` K )
5	1 2 3 4	islhp	|- ( K e. A -> ( W e. H <-> ( W e. B /\ W C .1. ) ) )
6	5	baibd	|- ( ( K e. A /\ W e. B ) -> ( W e. H <-> W C .1. ) )