let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NATPLUS or x in RATPLUS )
assume A1: x in NATPLUS ; :: thesis: x in RATPLUS
then reconsider y = x as Nat ;
0 < y by A1, NAT_LAT:def 6;
hence x in RATPLUS ; :: thesis: verum