:: deftheorem Def15 defines non-zero ORDINAL1:def 15 :
for R being Relation holds
( R is non-zero iff not 0 in rng R );