theorem actual_everyone_immoral_rejects_only_rich
theorem actual_everyone_immoral_rejects_only_rich
(logic_is_actual : LogicIsActual)
(everyone : A EveryPersonIsImmoral)
(someone_not_rich : A (∃ p : Person, ¬ (p is-rich)))
: A (¬ OnlyRichPeopleAreImmoral)