:: deftheorem defines NonZero STRUCT_0:def 17 :
for S being ZeroStr holds NonZero S = ([#] S) \ {(0. S)};