Metamath Proof Explorer


Theorem shoccl

Description: Closure of complement of Hilbert subspace. Part of Remark 3.12 of Beran p. 107. (Contributed by NM, 13-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion shoccl ( 𝐴S → ( ⊥ ‘ 𝐴 ) ∈ C )

Proof

Step Hyp Ref Expression
1 shss ( 𝐴S𝐴 ⊆ ℋ )
2 occl ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ∈ C )
3 1 2 syl ( 𝐴S → ( ⊥ ‘ 𝐴 ) ∈ C )