theorem Th23: :: RUSUB_7:23

for X being RealUnitarySpace
for M being non empty Subset of X holds M is Subset of (Ort_Comp (Ort_Comp M))