theorem actual_some_not_immoral_is_saying_not_every
theorem actual_some_not_immoral_is_saying_not_every
(logic_is_actual : LogicIsActual)
: A (SomeRichPersonIsNotImmoral ↔ NotEveryRichPersonIsImmoral)