reconsider i1 = n + 1 as Integer ;
reconsider q = 0 / i1 as Rational ;
q in RAT_with_denominator (n + 1) by Def2;
hence not RAT_with_denominator (n + 1) is empty ; :: thesis: verum