Description: Alternate proof of sels , requiring ax-sep but not using el (which
is proved from it as elALT ). (especially when the proof of el is
inlined in sels ). (Contributed by NM, 4-Jan-2002) Generalize from
the proof of elALT . (Revised by BJ, 3-Apr-2019)(Proof modification is discouraged.)(New usage is discouraged.)