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