theorem Th2: :: RAT_1:2

for x being object st x is rational holds
ex m, n being Integer st
( n > 0 & x = m / n ) by Th1;