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