let X be RealHilbertSpace; :: thesis: for M being non empty Subset of X st X is strict holds
( the carrier of (Ort_Comp (Ort_Comp M)) is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) & ex L being Subset of (TopSpaceNorm (RUSp2RNSp X)) st
( L = the carrier of (Lin M) & the carrier of (Ort_Comp (Ort_Comp M)) = Cl L ) & Lin M is Subspace of Ort_Comp (Ort_Comp M) )
let M be non empty Subset of X; :: thesis: ( X is strict implies ( the carrier of (Ort_Comp (Ort_Comp M)) is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) & ex L being Subset of (TopSpaceNorm (RUSp2RNSp X)) st
( L = the carrier of (Lin M) & the carrier of (Ort_Comp (Ort_Comp M)) = Cl L ) & Lin M is Subspace of Ort_Comp (Ort_Comp M) ) )
assume A1: X is strict ; :: thesis: ( the carrier of (Ort_Comp (Ort_Comp M)) is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) & ex L being Subset of (TopSpaceNorm (RUSp2RNSp X)) st
( L = the carrier of (Lin M) & the carrier of (Ort_Comp (Ort_Comp M)) = Cl L ) & Lin M is Subspace of Ort_Comp (Ort_Comp M) )
reconsider L = the carrier of (Lin M) as non empty Subset of X by RUSUB_1:def 1;
reconsider TL = L as Subset of (TopSpaceNorm (RUSp2RNSp X)) ;
A2: the carrier of (Ort_Comp (Ort_Comp M)) = Cl TL by A1, Lm7;
hence the carrier of (Ort_Comp (Ort_Comp M)) is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) ; :: thesis: ( ex L being Subset of (TopSpaceNorm (RUSp2RNSp X)) st
( L = the carrier of (Lin M) & the carrier of (Ort_Comp (Ort_Comp M)) = Cl L ) & Lin M is Subspace of Ort_Comp (Ort_Comp M) )
thus ex TL being Subset of (TopSpaceNorm (RUSp2RNSp X)) st
( TL = the carrier of (Lin M) & the carrier of (Ort_Comp (Ort_Comp M)) = Cl TL ) by A2; :: thesis: Lin M is Subspace of Ort_Comp (Ort_Comp M)
thus Lin M is Subspace of Ort_Comp (Ort_Comp M) by RUSUB_1:22, PRE_TOPC:18, A2; :: thesis: verum