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