for n being Nat holds INT , RAT_with_denominator (n + 1) are_equipotent