let A1, A2 be Subset of REAL ; :: thesis: ( ( for x being Real holds
( x in A1 iff ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & x = i / (2 |^ n) ) ) ) & ( for x being Real holds
( x in A2 iff ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & x = i / (2 |^ n) ) ) ) implies A1 = A2 )
assume that
A1: for x being Real holds
( x in A1 iff ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & x = i / (2 |^ n) ) ) and
A2: for x being Real holds
( x in A2 iff ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & x = i / (2 |^ n) ) ) ; :: thesis: A1 = A2
for a being set holds
( a in A1 iff a in A2 )

proof

let a be set ; :: thesis: ( a in A1 iff a in A2 )
thus ( a in A1 implies a in A2 ) :: thesis: ( a in A2 implies a in A1 )

proof

assume A3: a in A1 ; :: thesis: a in A2
then reconsider a = a as Real ;
ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) ) by A1, A3;
hence a in A2 by A2; :: thesis: verum

end;

assume A4: a in A2 ; :: thesis: a in A1
then reconsider a = a as Real ;
ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) ) by A2, A4;
hence a in A1 by A1; :: thesis: verum

end;

hence A1 = A2 by TARSKI:2; :: thesis: verum