Theorem psubssat

Description: A projective subspace consists of atoms. (Contributed by NM, 4-Nov-2011)

	Ref	Expression
Hypotheses	atpsub.a	|- A = ( Atoms ` K )
	atpsub.s	|- S = ( PSubSp ` K )
Assertion	psubssat	|- ( ( K e. B /\ X e. S ) -> X C_ A )

Proof

Step	Hyp	Ref	Expression
1		atpsub.a	|- A = ( Atoms ` K )
2		atpsub.s	|- S = ( PSubSp ` K )
3		eqid	|- ( le ` K ) = ( le ` K )
4		eqid	|- ( join ` K ) = ( join ` K )
5	3 4 1 2	ispsubsp	|- ( K e. B -> ( X e. S <-> ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. X ) ) ) )
6	5	simprbda	|- ( ( K e. B /\ X e. S ) -> X C_ A )