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: ( 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 consider i being Element of NAT such that
A4: ( 0 <= i & i <= 1 & x = i / 1 ) by A1, Def3;
thus ex i being Element of NAT st
( 0 <= i & i <= 1 & x = i ) by A4; :: thesis: verum

end;

( 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 A5: ( 0 <= i & i <= 1 & x = i ) ; :: thesis: x in dyadic 0
x = i / 1 by A5;
hence x in dyadic 0 by A1, A5, Def3; :: 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;

dyadic 0 = {0 ,1}

proof

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 & i <= 1 & x = i ) by A2, A7;
( 0 <= i & i <= 0 + 1 ) by A8;
then ( x = 0 or x = 1 ) by A8, 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

end;

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