let X be RealUnitarySpace; :: thesis: for M being non empty Subset of X holds M is Subset of (Ort_Comp (Ort_Comp M))
let M be non empty Subset of X; :: thesis: M is Subset of (Ort_Comp (Ort_Comp M))
reconsider N = the carrier of (Ort_Comp M) as non empty Subset of X by RUSUB_1:def 1;
A2: the carrier of (Ort_Comp (Ort_Comp M)) = the carrier of (Ort_Comp N) by Lm6
.= Ort_CompSet N by Lm5 ;
M c= Ort_CompSet (Ort_CompSet M)

proof

let x0 be object ; :: according to TARSKI:def 3 :: thesis: ( not x0 in M or x0 in Ort_CompSet (Ort_CompSet M) )
assume A3: x0 in M ; :: thesis: x0 in Ort_CompSet (Ort_CompSet M)
then reconsider x = x0 as Point of X ;
for y being Point of X st y in Ort_CompSet M holds
y .|. x = 0 by A3, Def1;
hence x0 in Ort_CompSet (Ort_CompSet M) by Def1; :: thesis: verum

end;

hence M is Subset of (Ort_Comp (Ort_Comp M)) by A2, Lm5; :: thesis: verum