:: deftheorem defines discerning NORMSP_0:def 5 :
for X being non empty N-ZeroStr holds
( X is discerning iff for x being Element of X st ||.x.|| = 0 holds
x = 0. X );