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