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 () c= the carrier of ()

let M, N be Subspace of X; :: thesis: ( the carrier of M c= the carrier of N implies the carrier of () c= the carrier of () )
assume A1: the carrier of M c= the carrier of N ; :: thesis: the carrier of () c= the carrier of ()
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of () or x in the carrier of () )
assume x in the carrier of () ; :: thesis: x in the carrier of ()
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:
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 () by RUSUB_5:def 3; :: thesis: verum