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

w,v are_orthogonal } ;

hence x in the carrier of (Ort_Comp M) by RUSUB_5:def 3; :: thesis: verum

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

then
x in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
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;assume y in M ; :: thesis: y,x are_orthogonal

then y in N by A1;

hence y,x are_orthogonal by A2; :: thesis: verum

w,v are_orthogonal } ;

hence x in the carrier of (Ort_Comp M) by RUSUB_5:def 3; :: thesis: verum