theorem Th20: :: RUSUB_1:20

for V, X being strict RealUnitarySpace st V is Subspace of X & X is Subspace of V holds
V = X