A1:
2 |^ 1 = 2
;

for x being object holds

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

for x being object holds

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

proof

hence
dyadic 1 = {0,(1 / 2),1}
by TARSKI:2; :: thesis: verum
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 )

end;A2: ( x in {0,(1 / 2),1} implies x in dyadic 1 )

proof

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

end;proof

hence
( x in dyadic 1 iff x in {0,(1 / 2),1} )
by A2; :: thesis: verum
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;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