Theorem spanss2

Description: A subset of Hilbert space is included in its span. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	spanss2	⊢ ( 𝐴 ⊆ ℋ → 𝐴 ⊆ ( span ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ssintub	⊢ 𝐴 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 }
2		spanval	⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )
3	1 2	sseqtrrid	⊢ ( 𝐴 ⊆ ℋ → 𝐴 ⊆ ( span ‘ 𝐴 ) )