let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in RATPLUS or x in REALPLUS )
assume x in RATPLUS ; :: thesis: x in REALPLUS
then reconsider y = x as positive Rational by Th2;
0 < y ;
hence x in REALPLUS by Th1; :: thesis: verum