theorem Th25: :: RUSUB_5:25

for V being RealUnitarySpace
for M being non empty Subset of V holds M c= the carrier of (Ort_Comp (Ort_Comp M))