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