defpred S1[ Element of RAT ] means ex i being Integer st $1 = i / n;
consider X being Subset of RAT such that
A1: for r being Element of RAT holds
( r in X iff S1[r] ) from SUBSET_1:sch 3();
 A2: for q being Rational holds
( q in X iff ex i being Integer st q = i / n )
proof
let q be Rational; :: thesis: ( q in X iff ex i being Integer st q = i / n )
reconsider q = q as Element of RAT by RAT_1:def 2;
( q in X iff ex i being Integer st q = i / n ) by A1;
hence ( q in X iff ex i being Integer st q = i / n ) ; :: thesis: verum
end;
take X ; :: thesis: for q being Rational holds
( q in X iff ex i being Integer st q = i / n )
thus for q being Rational holds
( q in X iff ex i being Integer st q = i / n ) by A2; :: thesis: verum