let i, j be Element of omega ; :: thesis: ( i,j are_relative_prime & j <> {} implies ( numerator (i / j) = i & denominator (i / j) = j ) )
assume i,j are_relative_prime ; :: thesis: ( not j <> {} or ( numerator (i / j) = i & denominator (i / j) = j ) )
then ( RED i,j = i & RED j,i = j ) by Th28;
hence ( not j <> {} or ( numerator (i / j) = i & denominator (i / j) = j ) ) by Th48; :: thesis: verum