Description: Alternate proof of elisset . This is essentially the same proof as
seen by inlining bj-denotes and bj-denoteslem . Use elissetv instead when sufficient (in particular when V is substituted for
_V ). (Contributed by BJ, 29-Apr-2019)(Proof modification is discouraged.)(New usage is discouraged.)