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 {0,(1 / 2),1} implies x in dyadic 1 )

proof

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

per cases ( x = 0 or x = 1 / 2 or x = 1 ) by A3, 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 A4: x = 1 ; :: thesis: x in dyadic 1

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

end;

end;

end;

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

proof

assume A5: 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
A6: 0 <= i and
A7: i <= 2 and
A8: x = i / 2 by A1, A5, Def3;
( i <= 1 or i = 1 + 1 ) by A7, NAT_1:8;
then ( i = 0 or i = 0 + 1 or i = 2 ) by A6, NAT_1:9;
hence x in {0,(1 / 2),1} by A8, ENUMSET1:def 1; :: thesis: verum

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