Description: This theorem is in fact a copy of com23 . It starts a series of
theorems named after wl-impchain-com-n.m . For more information see
there. (Contributed by Wolf Lammen, 12-Nov-2019)(New usage is discouraged.)(Proof modification is discouraged.)