theorem :: DUALSP04:30

for X being RealUnitarySpace
for M being Subspace of X
for N being non empty Subset of X st N = the carrier of (Ort_Comp M) holds
( N is linearly-closed & N is closed )