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 | |- ( A e. SH -> ( _|_ ` A ) e. CH ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | shss | |- ( A e. SH -> A C_ ~H ) |
|
| 2 | occl | |- ( A C_ ~H -> ( _|_ ` A ) e. CH ) |
|
| 3 | 1 2 | syl | |- ( A e. SH -> ( _|_ ` A ) e. CH ) |