let r be object ; :: thesis: ( r is Element of RATPLUS iff r is positive Rational )

hereby :: thesis: ( r is positive Rational implies r is Element of RATPLUS )

assume r is Element of RATPLUS ; :: thesis: r is positive Rational
then r in { r where r is positive Rational : verum } ;
then ex s being positive Rational st r = s ;
hence r is positive Rational ; :: thesis: verum

end;

assume r is positive Rational ; :: thesis: r is Element of RATPLUS
then r in { r where r is positive Rational : verum } ;
hence r is Element of RATPLUS ; :: thesis: verum