Description: Closure of complement of Hilbert subspace. Part of Remark 3.12 of Beran p. 107. (Contributed by NM, 22-Jul-2001) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | choccl | |- ( A e. CH -> ( _|_ ` A ) e. CH ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | chsh | |- ( A e. CH -> A e. SH ) |
|
| 2 | shoccl | |- ( A e. SH -> ( _|_ ` A ) e. CH ) |
|
| 3 | 1 2 | syl | |- ( A e. CH -> ( _|_ ` A ) e. CH ) |