|Description: Derivation of set.mm's
original ax-11o 1941 from ax-10 1678 and the shorter
ax-11 1624 that has replaced it.
An open problem is whether this theorem can be proved without relying on
ax-16 1927 or ax-17 1628 (given all of the original and new
versions of ax-4 1692
through ax-15 2105).
Another open problem is whether this theorem can be proved without
relying on ax-12o 1664.
Theorem ax11 1942 shows the reverse derivation of ax-11 1624 from ax-11o 1941.
Normally, ax11o 1940 should be used rather than ax-11o 1941, except by
theorems specifically studying the latter's properties. (Contributed by