defpred S₁[ set ] means ex i being Element of NAT st $1 in dyadic i;
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 a being Real holds
( a in b₁ iff ex n being Element of NAT st a in dyadic n ) ; :: thesis: verum