Description: Theorem 19.2 of Margaris p. 89. This corresponds to the axiom (D) of
modal logic (the other standard formulation being extru ). Note: This
proof is very different from Margaris' because we only have Tarski's FOL
axiom schemes available at this point. See the later 19.2g for a more
conventional proof of a more general result, which uses additional axioms.
The reverse implication is the defining property of effective nonfreeness
(see df-nf ). (Contributed by NM, 2-Aug-2017) Remove dependency on
ax-7 . (Revised by Wolf Lammen, 4-Dec-2017)