логика - Грешные и безгрешные

У меня не вызывает сомнений, что импликация $$ \begin {cases} \varnothing \notin \{P \cap Hs, \ P \setminus Hs\} \\ \forall x (x \in P \rightarrow (x \in Hs \leftrightarrow x \ is \ mortal.)) \\ \forall x (x \in P \rightarrow (x \ is \ sinful. \leftrightarrow x \ is \ mortal.)) \end {cases} \rightarrow \begin {cases} \forall x (x \in P \cap Hs \rightarrow x \ is \ sinful.) \\ \forall x (x \in P \setminus Hs \rightarrow x \ is \ unsinful.)) \end {cases} $$ верна, если верна эквиваленция "$% \neg(x \ is \ sinful.) \leftrightarrow x \ is \ unsinful.$%".

Доказательство

$% \begin {cases} \varnothing \notin \{P \cap Hs, \ P \setminus Hs\} \\ \forall x (x \in P \rightarrow (x \in Hs \leftrightarrow x \ is \ mortal.)) \\ \forall x (x \in P \rightarrow (x \ is \ sinful. \leftrightarrow x \ is \ mortal.)) \end {cases}$%

$%\Rightarrow \forall x (x \in P \rightarrow (x \in Hs \leftrightarrow x \ is \ mortal.) \wedge (x \ is \ sinful. \leftrightarrow x \ is \ mortal.)) $%

$%\Rightarrow \forall x (x \in P \rightarrow (x \in Hs \leftrightarrow x \ is \ sinful.)) $%

$%\Leftrightarrow \forall x (x \in P \rightarrow (x \in Hs \leftrightarrow x \ is \ sinful.)) \wedge \forall x (x \in P \rightarrow (x \in Hs \leftrightarrow x \ is \ sinful.))$%

$%\Leftrightarrow \forall x (x \in P \rightarrow (x \in Hs \leftrightarrow x \ is \ sinful.)) \wedge \forall x (x \in P \rightarrow (x \notin Hs \leftrightarrow x \ is \ unsinful.))$%

$%\Rightarrow \forall x (x \in P \rightarrow (x \in Hs \rightarrow x \ is \ sinful.)) \wedge \forall x (x \in P \rightarrow (x \notin Hs \rightarrow x \ is \ unsinful.))$%

$%\Leftrightarrow \forall x (x \in P \wedge x \in Hs \rightarrow x \ is \ sinful.) \wedge \forall x (x \in P \wedge x \notin Hs \rightarrow x \ is \ unsinful.)$%

$%\Leftrightarrow \forall x (x \in P \cap Hs \rightarrow x \ is \ sinful.) \wedge \forall x (x \in P \setminus Hs \rightarrow x \ is \ unsinful.)$%