set X = { r where r is positive Rational : verum } ;
A1: the positive Rational in { r where r is positive Rational : verum } ;
{ r where r is positive Rational : verum } c= REAL+

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { r where r is positive Rational : verum } or x in REAL+ )
assume x in { r where r is positive Rational : verum } ; :: thesis: x in REAL+
then ex r being positive Rational st x = r ;
hence x in REAL+ by REAL_1:1; :: thesis: verum

end;

hence { r where r is positive Rational : verum } is non empty Subset of REAL+ by A1; :: thesis: verum