let e be object ; :: thesis: ( e in 0 -SD iff e = 0 )
A1: Radix 0 = 1 by POWER:24;
hereby :: thesis: ( e = 0 implies e in 0 -SD )
assume e in 0 -SD ; :: thesis: e = 0
then ex b being Element of INT st
( e = b & b <= 0 & b >= 0 ) by A1;
hence e = 0 ; :: thesis: verum
end;
assume A2: e = 0 ; :: thesis: e in 0 -SD
then e is Element of INT by INT_1:def 2;
hence e in 0 -SD by A1, A2; :: thesis: verum