theorem RHS11b: :: DUALSP04:7

for X being RealUnitarySpace holds
( X is complete iff RUSp2RNSp X is complete )