A1:
2 |^ 0 = 1
by NEWTON:4;

A2: for x being Real holds

( x in dyadic 0 iff ex i being Nat st

( i <= 1 & x = i ) )

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

A2: for x being Real holds

( x in dyadic 0 iff ex i being Nat st

( i <= 1 & x = i ) )

proof

for x being object holds
let x be Real; :: thesis: ( x in dyadic 0 iff ex i being Nat st

( i <= 1 & x = i ) )

A3: ( ex i being Nat st

( i <= 1 & x = i ) implies x in dyadic 0 )

( i <= 1 & x = i ) )

( i <= 1 & x = i ) ) by A3; :: thesis: verum

end;( i <= 1 & x = i ) )

A3: ( ex i being Nat st

( i <= 1 & x = i ) implies x in dyadic 0 )

proof

( x in dyadic 0 implies ex i being Nat st
given i being Nat such that A4:
i <= 1
and

A5: x = i ; :: thesis: x in dyadic 0

x = i / 1 by A5;

hence x in dyadic 0 by A1, A4, Def1; :: thesis: verum

end;A5: x = i ; :: thesis: x in dyadic 0

x = i / 1 by A5;

hence x in dyadic 0 by A1, A4, Def1; :: thesis: verum

( i <= 1 & x = i ) )

proof

hence
( x in dyadic 0 iff ex i being Nat st
assume
x in dyadic 0
; :: thesis: ex i being Nat st

( i <= 1 & x = i )

then ex i being Nat st

( i <= 1 & x = i / 1 ) by A1, Def1;

hence ex i being Nat st

( i <= 1 & x = i ) ; :: thesis: verum

end;( i <= 1 & x = i )

then ex i being Nat st

( i <= 1 & x = i / 1 ) by A1, Def1;

hence ex i being Nat st

( i <= 1 & x = i ) ; :: thesis: verum

( i <= 1 & x = i ) ) by A3; :: thesis: verum

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

proof

hence
dyadic 0 = {0,1}
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in dyadic 0 iff x in {0,1} )

A6: ( x in dyadic 0 implies x in {0,1} )

end;A6: ( x in dyadic 0 implies x in {0,1} )

proof

( x in {0,1} implies x in dyadic 0 )
assume A7:
x in dyadic 0
; :: thesis: x in {0,1}

then reconsider x = x as Real ;

consider i being Nat such that

A8: i <= 1 and

A9: x = i by A2, A7;

i <= 0 + 1 by A8;

then ( x = 0 or x = 1 ) by A9, NAT_1:9;

hence x in {0,1} by TARSKI:def 2; :: thesis: verum

end;then reconsider x = x as Real ;

consider i being Nat such that

A8: i <= 1 and

A9: x = i by A2, A7;

i <= 0 + 1 by A8;

then ( x = 0 or x = 1 ) by A9, NAT_1:9;

hence x in {0,1} by TARSKI:def 2; :: thesis: verum

proof

hence
( x in dyadic 0 iff x in {0,1} )
by A6; :: thesis: verum
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;then ( x = 0 or x = 1 ) by TARSKI:def 2;

hence x in dyadic 0 by A2; :: thesis: verum