let A1, A2 be Subset of REAL; :: thesis: ( ( 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) ) ) ; :: thesis: A1 = A2

for a being object holds

( a in A1 iff a in A2 )

( 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) ) ) ; :: thesis: A1 = A2

for a being object holds

( a in A1 iff a in A2 )

proof

hence
A1 = A2
by TARSKI:2; :: thesis: verum
let a be object ; :: thesis: ( a in A1 iff a in A2 )

thus ( a in A1 implies a in A2 ) :: thesis: ( a in A2 implies 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; :: thesis: verum

end;thus ( a in A1 implies a in A2 ) :: thesis: ( a in A2 implies a in A1 )

proof

assume A5:
a in A2
; :: thesis: a in A1
assume A4:
a in A1
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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; :: thesis: verum