for X being RealUnitarySpace
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)