let a, b be natural Ordinal; :: thesis: ( a,b are_coprime implies RED (a,b) = a )
assume a,b are_coprime ; :: thesis: RED (a,b) = a
then a hcf b = 1 by Th20;
hence RED (a,b) = a by ORDINAL3:71; :: thesis: verum