A1: 2 |^ 1 = 2 by NEWTON:10;
for x being set holds
( x in dyadic 1 iff x in {0 ,(1 / 2),1} )

proof

let x be set ; :: thesis: ( x in dyadic 1 iff x in {0 ,(1 / 2),1} )
A2: ( x in dyadic 1 implies x in {0 ,(1 / 2),1} )

proof

assume A3: x in dyadic 1 ; :: thesis: x in {0 ,(1 / 2),1}
then reconsider x = x as Real ;
consider i being Element of NAT such that
A4: ( 0 <= i & i <= 2 & x = i / 2 ) by A1, A3, Def3;
( 0 <= i & ( i <= 1 or i = 1 + 1 ) ) by A4, NAT_1:8;
then ( i = 0 or i = 0 + 1 or i = 2 ) by NAT_1:9;
hence x in {0 ,(1 / 2),1} by A4, ENUMSET1:def 1; :: thesis: verum

end;

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

proof

assume A5: x in {0 ,(1 / 2),1} ; :: thesis: x in dyadic 1

per cases ( x = 0 or x = 1 / 2 or x = 1 ) by A5, ENUMSET1:def 1;

suppose x = 0 ; :: thesis: x in dyadic 1

then x = 0 / 2 ;
hence x in dyadic 1 by A1, Def3; :: thesis: verum

end;

suppose x = 1 / 2 ; :: thesis: x in dyadic 1

hence x in dyadic 1 by A1, Def3; :: thesis: verum

end;

suppose A6: x = 1 ; :: thesis: x in dyadic 1

then reconsider x = x as Real ;
x = 2 / 2 by A6;
hence x in dyadic 1 by A1, Def3; :: thesis: verum

end;

end;

end;

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

end;

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