:: deftheorem defines with_zero QUANTAL1:def 4 :
for IT being non empty multMagma holds
( IT is with_zero iff ( IT is with_left-zero & IT is with_right-zero ) );