let a, b be natural Ordinal; :: thesis: ( a hcf b = {} implies a = {} )
a hcf b divides a by Def5;
then a = (a hcf b) *^ (a div^ (a hcf b)) by Th7;
hence ( a hcf b = {} implies a = {} ) by ORDINAL2:35; :: thesis: verum