Theorem psubcliN

Description: Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	psubclset.a	|- A = ( Atoms ` K )
	psubclset.p	|- ._|_ = ( _|_P ` K )
	psubclset.c	|- C = ( PSubCl ` K )
Assertion	psubcliN	|- ( ( K e. D /\ X e. C ) -> ( X C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) )

Proof

Step	Hyp	Ref	Expression
1		psubclset.a	|- A = ( Atoms ` K )
2		psubclset.p	|- ._|_ = ( _|_P ` K )
3		psubclset.c	|- C = ( PSubCl ` K )
4	1 2 3	ispsubclN	|- ( K e. D -> ( X e. C <-> ( X C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) )
5	4	biimpa	|- ( ( K e. D /\ X e. C ) -> ( X C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) )