let X be RealUnitarySpace; :: thesis: for M being Subspace of X holds the carrier of M c= the carrier of (Ort_Comp (Ort_Comp M))
let M be Subspace of X; :: thesis: the carrier of M c= the carrier of (Ort_Comp (Ort_Comp M))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of M or x in the carrier of (Ort_Comp (Ort_Comp M)) )
assume AS: x in the carrier of M ; :: thesis: x in the carrier of (Ort_Comp (Ort_Comp M))
then A1: x in M ;
the carrier of M c= the carrier of X by RUSUB_1:def 1;
then reconsider x = x as VECTOR of X by AS;
for y being VECTOR of X st y in Ort_Comp M holds
x,y are_orthogonal

proof

let y be VECTOR of X; :: thesis: ( y in Ort_Comp M implies x,y are_orthogonal )
assume y in Ort_Comp M ; :: thesis: x,y are_orthogonal
then y in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } by RUSUB_5:def 3;
then ex v being VECTOR of X st
( y = v & ( for w being VECTOR of X st w in M holds
w,v are_orthogonal ) ) ;
hence x,y are_orthogonal by A1; :: thesis: verum

end;

then x in { v where v is VECTOR of X : for w being VECTOR of X st w in Ort_Comp M holds
w,v are_orthogonal } ;
hence x in the carrier of (Ort_Comp (Ort_Comp M)) by RUSUB_5:def 3; :: thesis: verum