defpred S₁[ Rational] means |.(r - $1).| < 1 / ((sqrt 5) * ((denominator $1) |^ 2));
{ p where p is Rational : S₁[p] } c= RAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { p where p is Rational : S₁[p] } or y in RAT )
assume y in { p where p is Rational : S₁[p] } ; :: thesis: y in RAT
then ex r being Rational st
( y = r & S₁[r] ) ;
hence y in RAT by RAT_1:def 2; :: thesis: verum

end;

hence { p where p is Rational : |.(r - p).| < 1 / ((sqrt 5) * ((denominator p) |^ 2)) } is Subset of RAT ; :: thesis: verum