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:71; :: thesis: verum