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