defpred S₁[ set ] means ex i being Element of NAT st
( i <= 2 |^ n & $1 = i / (2 |^ n) );
ex X being Subset of REAL st
for x being Real holds
( x in X iff S₁[x] ) from SUBSET_1:sch 3();
hence ex b₁ being Subset of REAL st
for x being Real holds
( x in b₁ iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) ; :: thesis: verum