reconsider a = 0 , b = 1 as Integer ;
take x = a / b; :: thesis: ( x is Real & x is rational )
thus x is Real ; :: thesis: x is rational
thus x in RAT by Def1; :: according to RAT_1:def 2 :: thesis: verum