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

proof

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

proof

given i being Element of NAT such that A4: ( 0 <= i & i <= 1 ) and
A5: x = i ; :: thesis: x in dyadic 0
x = i / 1 by A5;
hence x in dyadic 0 by A1, A4, Def3; :: thesis: verum

end;

( x in dyadic 0 implies ex i being Element of NAT st
( 0 <= i & i <= 1 & x = i ) )

proof

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

end;

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

end;

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

proof

let x be set ; :: 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 Element of NAT such that
A8: 0 <= i and
A9: i <= 1 and
A10: x = i by A2, A7;
i <= 0 + 1 by A9;
then ( x = 0 or x = 1 ) by A8, A10, 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