defpred S₁[ set ] means ex i being Nat st $1 in dyadic i;
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 a being Real holds
( a in X iff ex n being Nat st a in dyadic n )
let a be Real; :: thesis: ( a in X iff ex n being Nat st a in dyadic n )
reconsider a = a as Element of REAL by XREAL_0:def 1;
( a in X iff S₁[a] ) by A1;
hence ( a in X iff ex n being Nat st a in dyadic n ) ; :: thesis: verum