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

take x = a / b; :: thesis: x is rational

thus x in RAT by Def1; :: according to RAT_1:def 2 :: thesis: verum