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