for V being RealUnitarySpace
for x being set holds
( x in (0). V iff x = 0. V ) by Lm1;