Theorem psubclssatN

Description: A closed projective subspace is a set of atoms. (Contributed by NM, 25-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	psubclssat.a	|- A = ( Atoms ` K )
	psubclssat.c	|- C = ( PSubCl ` K )
Assertion	psubclssatN	|- ( ( K e. D /\ X e. C ) -> X C_ A )

Proof

Step	Hyp	Ref	Expression
1		psubclssat.a	|- A = ( Atoms ` K )
2		psubclssat.c	|- C = ( PSubCl ` K )
3		eqid	|- ( _|_P ` K ) = ( _|_P ` K )
4	1 3 2	psubcliN	|- ( ( K e. D /\ X e. C ) -> ( X C_ A /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) )
5	4	simpld	|- ( ( K e. D /\ X e. C ) -> X C_ A )