theorem Th4: :: MESFUNC1:4

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