defpred S₁[ object ] means ex i being Integer st $1 = i / (2 |^ n);
consider IT being set such that
A1: for o being object holds
( o in IT iff ( o in DYADIC & S₁[o] ) ) from XBOOLE_0:sch 1();
IT c= DYADIC

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in IT or o in DYADIC )
assume o in IT ; :: thesis: o in DYADIC
hence o in DYADIC by A1; :: thesis: verum

end;

then reconsider IT = IT as Subset of DYADIC ;
take IT ; :: thesis: for d being Dyadic holds
( d in IT iff ex i being Integer st d = i / (2 |^ n) )
let d be Dyadic; :: thesis: ( d in IT iff ex i being Integer st d = i / (2 |^ n) )
thus ( d in IT implies ex i being Integer st d = i / (2 |^ n) ) by A1; :: thesis: ( ex i being Integer st d = i / (2 |^ n) implies d in IT )
given i being Integer such that A2: d = i / (2 |^ n) ; :: thesis: d in IT
d in DYADIC by Def3;
hence d in IT by A2, A1; :: thesis: verum