let X be RealUnitarySpace; :: thesis: for M, N being Subspace of X st the carrier of M c= the carrier of N holds
the carrier of (Ort_Comp N) c= the carrier of (Ort_Comp M)
let M, N be Subspace of X; :: thesis: ( the carrier of M c= the carrier of N implies the carrier of (Ort_Comp N) c= the carrier of (Ort_Comp M) )
assume A1: the carrier of M c= the carrier of N ; :: thesis: the carrier of (Ort_Comp N) c= the carrier of (Ort_Comp M)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (Ort_Comp N) or x in the carrier of (Ort_Comp M) )
assume x in the carrier of (Ort_Comp N) ; :: thesis: x in the carrier of (Ort_Comp M)
then x in { v where v is VECTOR of X : for w being VECTOR of X st w in N holds
w,v are_orthogonal } by RUSUB_5:def 3;
then A2: ex v1 being VECTOR of X st
( x = v1 & ( for w being VECTOR of X st w in N holds
w,v1 are_orthogonal ) ) ;
then reconsider x = x as VECTOR of X ;
for y being VECTOR of X st y in M holds
y,x are_orthogonal

proof

let y be VECTOR of X; :: thesis: ( y in M implies y,x are_orthogonal )
assume y in M ; :: thesis: y,x are_orthogonal
then y in N by A1;
hence y,x are_orthogonal by A2; :: thesis: verum

end;

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