theorem Th12: :: GAUSSINT:12

for p being G_RAT ex x, y being G_INTEG st
( y <> 0 & p = x / y )