A1: 2 |^ 0 = 1 by NEWTON:4;
thus INT c= DYADIC 0 :: according to XBOOLE_0:def 10 :: thesis: DYADIC 0 c= INT

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in INT or o in DYADIC 0 )
assume o in INT ; :: thesis: o in DYADIC 0
then reconsider o = o as Integer ;
o = o / (2 |^ 0) by A1;
hence o in DYADIC 0 by Def4; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in DYADIC 0 or o in INT )
assume o in DYADIC 0 ; :: thesis: o in INT
then ex i being Integer st o = i / (2 |^ 0) by Def4;
hence o in INT by A1, INT_1:def 2; :: thesis: verum