theorem Th26: :: RUSUB_5:26

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