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