for a, b being natural Ordinal st ( a <> {} or b <> {} ) holds
ex c, d1, d2 being natural Ordinal st
( d1,d2 are_coprime & a = c *^ d1 & b = c *^ d2 )