Metamath Proof Explorer

Theorem choccl

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 C A C


Step Hyp Ref Expression
1 chsh A C A S
2 shoccl A S A C
3 1 2 syl A C A C