let V be RealUnitarySpace; :: thesis: for M, N being non empty Subset of V st M c= N holds
the carrier of (Ort_Comp N) c= the carrier of (Ort_Comp M)
let M, N be non empty Subset of V; :: thesis: ( M c= N implies the carrier of (Ort_Comp N) c= the carrier of (Ort_Comp M) )
assume A1: M c= 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 V : for w being VECTOR of V st w in N holds
w,v are_orthogonal } by Def4;
then A2: ex v1 being VECTOR of V st
( x = v1 & ( for w being VECTOR of V st w in N holds
w,v1 are_orthogonal ) ) ;
then reconsider x = x as VECTOR of V ;
for y being VECTOR of V st y in M holds
y,x are_orthogonal by A1, A2;
then x in { v where v is VECTOR of V : for w being VECTOR of V st w in M holds
w,v are_orthogonal } ;
hence x in the carrier of (Ort_Comp M) by Def4; :: thesis: verum