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