take x = 0 / 1; :: thesis: x is rational
thus x in RAT by Def1; :: according to RAT_1:def 2 :: thesis: verum