:: deftheorem defines non-zero STRUCT_0:def 15 :
for X being set
for S being ZeroStr
for R being Relation of X, the carrier of S holds
( R is non-zero iff not 0. S in rng R );