:: deftheorem Def2 defines with_zero FREEALG:def 2 :
for IT being Relation holds
( not IT is with_zero iff not 0 in rng IT );