let V be RealUnitarySpace; :: thesis: for M being non empty Subset of V holds M c= the carrier of (Ort_Comp (Ort_Comp M))
let M be non empty Subset of V; :: thesis: M c= the carrier of (Ort_Comp (Ort_Comp M))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in M or x in the carrier of (Ort_Comp (Ort_Comp M)) )
assume A1: x in M ; :: thesis: x in the carrier of (Ort_Comp (Ort_Comp M))
then reconsider x = x as VECTOR of V ;
for y being VECTOR of V st y in Ort_Comp M holds
x,y are_orthogonal

proof

let y be VECTOR of V; :: 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 the carrier of (Ort_Comp M) ;
then y in { v where v is VECTOR of V : for w being VECTOR of V st w in M holds
w,v are_orthogonal } by Def4;
then ex v being VECTOR of V st
( y = v & ( for w being VECTOR of V 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 V : for w being VECTOR of V st w in Ort_Comp M holds
w,v are_orthogonal } ;
hence x in the carrier of (Ort_Comp (Ort_Comp M)) by Def3; :: thesis: verum