theorem actual_more_moral_asymmetric
theorem actual_more_moral_asymmetric
(logic_is_actual : LogicIsActual)
(coherent : A MoralComparisonIsCoherent)
: ∀ (a b : MoralCharacter), A (a.val more-moral-than b.val) → A ¬b.val more-moral-than a.val