let A1, A2 be Subset of REAL; ( ( for x being Real holds
( x in A1 iff ex i being Nat st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) & ( for x being Real holds
( x in A2 iff ex i being Nat st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) implies A1 = A2 )
assume that
A2:
for x being Real holds
( x in A1 iff ex i being Nat st
( i <= 2 |^ n & x = i / (2 |^ n) ) )
and
A3:
for x being Real holds
( x in A2 iff ex i being Nat st
( i <= 2 |^ n & x = i / (2 |^ n) ) )
; A1 = A2
for a being object holds
( a in A1 iff a in A2 )
proof
let a be
object ;
( a in A1 iff a in A2 )
thus
(
a in A1 implies
a in A2 )
( a in A2 implies a in A1 )proof
assume A4:
a in A1
;
a in A2
then reconsider a =
a as
Real ;
ex
i being
Nat st
(
i <= 2
|^ n &
a = i / (2 |^ n) )
by A2, A4;
hence
a in A2
by A3;
verum
end;
assume A5:
a in A2
;
a in A1
then reconsider a =
a as
Real ;
ex
i being
Nat st
(
i <= 2
|^ n &
a = i / (2 |^ n) )
by A3, A5;
hence
a in A1
by A2;
verum
end;
hence
A1 = A2
by TARSKI:2; verum