theorem :: DUALSP04:28

for X being RealUnitarySpace
for M being Subspace of X holds the carrier of M c= the carrier of (Ort_Comp (Ort_Comp M))