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

proof

let x be object ; :: 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, Def1; :: thesis: verum

end;

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

hence x in dyadic 1 by A1, Def1; :: 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, Def1; :: 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 Nat such that
A6: i <= 2 and
A7: x = i / 2 by A1, A5, Def1;
not not i = 0 & ... & not i = 2 by A6;
hence x in {0,(1 / 2),1} by A7, 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