命題
K を実数体または複素数体とする。
E を K 上の分離的な前Hilbert空間(過去スレ010の598)とする。
E の部分集合 S が完全(>>149)なら S^⊥ = {0} である。
ここで、S^⊥ は S の直交補空間(過去スレ010の601)である。

証明
x を S^⊥ の任意の元とする。
S が生成する E の代数的な線型部分空間を M とする。
M の閉包は E だから M の元の列 (x_n), n = 1, 2, ... で
lim x_n = x となるものが存在する。
x ∈ S^⊥ だからすべての n に対して <x, x_n> = 0 である。
>>150 より、(z, w) → <z, w> は連続だから
<x, x> = 0 である。
E は分離的だから x = 0 である。
よって、S^⊥ = {0} である。
証明終