A1: 2 |^ 0 = 1 by NEWTON:4;
A2: for x being Real holds
( x in dyadic 0 iff ex i being Nat st
( i <= 1 & x = i ) )

proof

let x be Real; :: thesis: ( x in dyadic 0 iff ex i being Nat st
( i <= 1 & x = i ) )
A3: ( ex i being Nat st
( i <= 1 & x = i ) implies x in dyadic 0 )

proof

given i being Nat such that A4: i <= 1 and
A5: x = i ; :: thesis: x in dyadic 0
x = i / 1 by A5;
hence x in dyadic 0 by A1, A4, Def1; :: thesis: verum

end;

( x in dyadic 0 implies ex i being Nat st
( i <= 1 & x = i ) )

proof

assume x in dyadic 0 ; :: thesis: ex i being Nat st
( i <= 1 & x = i )
then ex i being Nat st
( i <= 1 & x = i / 1 ) by A1, Def1;
hence ex i being Nat st
( i <= 1 & x = i ) ; :: thesis: verum

end;

hence ( x in dyadic 0 iff ex i being Nat st
( i <= 1 & x = i ) ) by A3; :: thesis: verum

end;

for x being object holds
( x in dyadic 0 iff x in {0,1} )

proof

let x be object ; :: thesis: ( x in dyadic 0 iff x in {0,1} )
A6: ( x in dyadic 0 implies x in {0,1} )

proof

assume A7: x in dyadic 0 ; :: thesis: x in {0,1}
then reconsider x = x as Real ;
consider i being Nat such that
A8: i <= 1 and
A9: x = i by A2, A7;
i <= 0 + 1 by A8;
then ( x = 0 or x = 1 ) by A9, NAT_1:9;
hence x in {0,1} by TARSKI:def 2; :: thesis: verum

end;

( x in {0,1} implies x in dyadic 0 )

proof

assume x in {0,1} ; :: thesis: x in dyadic 0
then ( x = 0 or x = 1 ) by TARSKI:def 2;
hence x in dyadic 0 by A2; :: thesis: verum

end;

hence ( x in dyadic 0 iff x in {0,1} ) by A6; :: thesis: verum

end;

hence dyadic 0 = {0,1} by TARSKI:2; :: thesis: verum