:: deftheorem Def1 defines without_zero MEASURE6:def 2 :
for X being set holds
( X is without_zero iff not 0 in X );