defpred S_{1}[ 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_{1}[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_{1}[a] )
by A1;

hence ( a in X iff ex n being Nat st a in dyadic n ) ; :: thesis: verum

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 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

hence ( a in X iff ex n being Nat st a in dyadic n ) ; :: thesis: verum