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	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	psubclssat.c	⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion	psubclssatN	⊢ ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		psubclssat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		psubclssat.c	⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
3		eqid	⊢ ( ⊥𝑃 ‘ 𝐾 ) = ( ⊥𝑃 ‘ 𝐾 )
4	1 3 2	psubcliN	⊢ ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶 ) → ( 𝑋 ⊆ 𝐴 ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) )
5	4	simpld	⊢ ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ⊆ 𝐴 )