|Description: Derivation of set.mm's
original ax-11o 1512 from the shorter ax-11 1268 that
has replaced it.
An open problem is whether this theorem can be proved without relying on
ax-16 1503 or ax-17 1285.
Another open problem is whether this theorem can be proved without
relying on ax-12 1272 (see note in a12study 1850).
Theorem ax11 1834 shows the reverse derivation of ax-11 1268 from ax-11o 1512.
Normally, ax11o 1511 should be used rather than ax-11o 1512, except by
theorems specifically studying the latter's properties. (Contributed by