defpred S_{1}[ set ] means ex i being Nat st

( i <= 2 |^ n & $1 = i / (2 |^ n) );

consider X being Subset of REAL such that

A1: for x being Element of REAL holds

( x in X iff S_{1}[x] )
from SUBSET_1:sch 3();

take X ; :: thesis: for x being Real holds

( x in X iff ex i being Nat st

( i <= 2 |^ n & x = i / (2 |^ n) ) )

let x be Real; :: thesis: ( x in X iff ex i being Nat st

( i <= 2 |^ n & x = i / (2 |^ n) ) )

reconsider x = x as Element of REAL by XREAL_0:def 1;

( x in X iff S_{1}[x] )
by A1;

hence ( x in X iff ex i being Nat st

( i <= 2 |^ n & x = i / (2 |^ n) ) ) ; :: thesis: verum

( i <= 2 |^ n & $1 = i / (2 |^ n) );

consider X being Subset of REAL such that

A1: for x being Element of REAL holds

( x in X iff S

take X ; :: thesis: for x being Real holds

( x in X iff ex i being Nat st

( i <= 2 |^ n & x = i / (2 |^ n) ) )

let x be Real; :: thesis: ( x in X iff ex i being Nat st

( i <= 2 |^ n & x = i / (2 |^ n) ) )

reconsider x = x as Element of REAL by XREAL_0:def 1;

( x in X iff S

hence ( x in X iff ex i being Nat st

( i <= 2 |^ n & x = i / (2 |^ n) ) ) ; :: thesis: verum