theorem Th25: :: RUSUB_1:25

for V being RealUnitarySpace
for W1, W2 being strict Subspace of V st ( for v being VECTOR of V holds
( v in W1 iff v in W2 ) ) holds
W1 = W2