for a, b being natural Ordinal st b <> {} holds
( a hcf b <> {} & b div^ (a hcf b) <> {} )