defpred S_{1}[ Rational] means |.(r - $1).| < 1 / ((sqrt 5) * ((denominator $1) |^ 2));

{ p where p is Rational : S_{1}[p] } c= RAT

{ p where p is Rational : S

proof

hence
{ p where p is Rational : |.(r - p).| < 1 / ((sqrt 5) * ((denominator p) |^ 2)) } is Subset of RAT
; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { p where p is Rational : S_{1}[p] } or y in RAT )

assume y in { p where p is Rational : S_{1}[p] }
; :: thesis: y in RAT

then ex r being Rational st

( y = r & S_{1}[r] )
;

hence y in RAT by RAT_1:def 2; :: thesis: verum

end;assume y in { p where p is Rational : S

then ex r being Rational st

( y = r & S

hence y in RAT by RAT_1:def 2; :: thesis: verum