let a be natural Ordinal; :: thesis: ( RED (a,1) = a & RED (1,a) = 1 )
a,1 are_relative_prime by Th6;
then a hcf 1 = 1 by Th25;
hence ( RED (a,1) = a & RED (1,a) = 1 ) by ORDINAL3:71; :: thesis: verum