:: deftheorem defines 0. STRUCT_0:def 6 :
for S being ZeroStr holds 0. S = the ZeroF of S;