let a, b be natural Ordinal; :: thesis: ( a,b are_relative_prime implies RED a,b = a )
assume a,b are_relative_prime ; :: thesis: RED a,b = a
then a hcf b = 1 by Th25;
hence RED a,b = a by ORDINAL3:84; :: thesis: verum