let X be RealHilbertSpace; :: thesis: for M, L being non empty Subset of X
for TL being Subset of (TopSpaceNorm (RUSp2RNSp X)) st X is strict & L = the carrier of (Lin M) & TL = L holds
the carrier of (Ort_Comp (Ort_Comp M)) = Cl TL
let M, L be non empty Subset of X; :: thesis: for TL being Subset of (TopSpaceNorm (RUSp2RNSp X)) st X is strict & L = the carrier of (Lin M) & TL = L holds
the carrier of (Ort_Comp (Ort_Comp M)) = Cl TL
let TL be Subset of (TopSpaceNorm (RUSp2RNSp X)); :: thesis: ( X is strict & L = the carrier of (Lin M) & TL = L implies the carrier of (Ort_Comp (Ort_Comp M)) = Cl TL )
assume A1: ( X is strict & L = the carrier of (Lin M) & TL = L ) ; :: thesis: the carrier of (Ort_Comp (Ort_Comp M)) = Cl TL
TL c= Cl TL by PRE_TOPC:18;
then reconsider CTL = Cl TL as non empty Subset of X by A1;
A3: L c= CTL by A1, PRE_TOPC:18;
consider CLM being strict Subspace of X such that
A4: CTL = the carrier of CLM by RUSUB_1:29, Th27, A1;
M c= CTL

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in M or z in CTL )
assume A5: z in M ; :: thesis: z in CTL
reconsider x = z as set by TARSKI:1;
x in Lin M by RUSUB_3:2, A5;
hence z in CTL by A3, A1, STRUCT_0:def 5; :: thesis: verum

end;

then Ort_Comp CTL is Subspace of Ort_Comp M by Th24;
then A6: the carrier of (Ort_Comp CTL) c= the carrier of (Ort_Comp M) by RUSUB_1:def 1;
reconsider CL = the carrier of (Ort_Comp CTL), CM = the carrier of (Ort_Comp M) as non empty Subset of X by RUSUB_1:def 1;
reconsider CCM = the carrier of (Ort_Comp (Ort_Comp M)) as non empty Subset of X by RUSUB_1:def 1;
reconsider TCCM = CCM as non empty Subset of (TopSpaceNorm (RUSp2RNSp X)) ;
A7: Ort_Comp CM is Subspace of Ort_Comp CL by Th24, A6;
A8: Ort_Comp (Ort_Comp M) = Ort_Comp CM by Lm6;
Ort_Comp (Ort_Comp M) is Subspace of Ort_Comp (Ort_Comp CTL) by A7, A8, Lm6;
then Ort_Comp (Ort_Comp M) is Subspace of Ort_Comp (Ort_Comp CLM) by A4, Lm6;
then A11: Ort_Comp (Ort_Comp M) is Subspace of CLM by Th26, A1, A4;
M is Subset of (Ort_Comp (Ort_Comp M)) by Th23;
then Lin M is Subspace of Lin CCM by RUSUB_3:7;
then Lin M is Subspace of Ort_Comp (Ort_Comp M) by RUSUB_3:5;
then TL c= CCM by A1, RUSUB_1:def 1;
hence the carrier of (Ort_Comp (Ort_Comp M)) = Cl TL by TOPS_1:5, Th22, A8, A11, A4, RUSUB_1:def 1; :: thesis: verum