defpred S₁[ 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₁[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₁[x] ) by A1;
hence ( x in X iff ex i being Nat st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) ; :: thesis: verum