let a, b be natural Ordinal; :: thesis: (RED (a,b)) *^ (a hcf b) = a
a hcf b divides a by Def5;
hence (RED (a,b)) *^ (a hcf b) = a by Th7; :: thesis: verum