Theorem islpln4

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

	Ref	Expression
Hypotheses	lplnset.b	|- B = ( Base ` K )
	lplnset.c	|- C = (
	lplnset.n	|- N = ( LLines ` K )
	lplnset.p	|- P = ( LPlanes ` K )
Assertion	islpln4	|- ( ( K e. A /\ X e. B ) -> ( X e. P <-> E. y e. N y C X ) )

Proof

Step	Hyp	Ref	Expression
1		lplnset.b	|- B = ( Base ` K )
2		lplnset.c	|- C = (
3		lplnset.n	|- N = ( LLines ` K )
4		lplnset.p	|- P = ( LPlanes ` K )
5	1 2 3 4	islpln	|- ( K e. A -> ( X e. P <-> ( X e. B /\ E. y e. N y C X ) ) )
6	5	baibd	|- ( ( K e. A /\ X e. B ) -> ( X e. P <-> E. y e. N y C X ) )