let n be number ; :: thesis: ( n is rational implies n is real )
assume n in RAT ; :: according to RAT_1:def 2 :: thesis: n is real
hence n in REAL by NUMBERS:12; :: according to XREAL_0:def 1 :: thesis: verum