:: deftheorem Def16 defines with_zero ORDINAL1:def 16 :
for X being set holds
( X is with_zero iff 0 in X );