:: deftheorem defines zero STRUCT_0:def 12 :
for S being ZeroStr
for x being Element of S holds
( x is zero iff x = 0. S );