логика - Грехопадение

Пусть $%P$% - множество людей, $%Hs$% - множество организмов вида Homo sapiens, $%T$% - время.

Вопрос: Верна ли следующая импликация

$$\begin {cases} \forall t_1 \forall t_2 (\{t_1, t_2\} \subseteq T \rightarrow (\neg(t_1 < t_2) \leftrightarrow t_1 \geq t_2))\\ \begin {cases} \forall x (x \in P \rightarrow (x \in Hs \leftrightarrow x \ is \ mortal.) \wedge (x \ is \ mortal. \leftrightarrow x \ is \ sinful.)) \\ \exists t_s (t_s \in T \wedge \forall t (t \in T \rightarrow (t \geq t_s \leftrightarrow Hs \neq \varnothing))) \end {cases} \end{cases}$$

$$\ \ \rightarrow \exists t_s (t_s \in T \wedge \forall t (t \in T \rightarrow \begin {cases} t < t_s \rightarrow \forall x (x \in P \rightarrow x \ is \ unsinful.) \\ t \geq t_s \rightarrow \exists x (x \in P \wedge x \ is \ sinful.) \end {cases})) ?$$

Примечание

$%1. \ $%«$%Hs \neq \varnothing \Leftrightarrow \exists x (x \in Hs)$%», тогда как «$%Hs = \varnothing \Leftrightarrow \forall x (x \notin Hs)$%».

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

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

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

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

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

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

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

$%\Leftrightarrow \ Hs = \varnothing \rightarrow \forall x (x \in P \rightarrow x \ is \ unsinful.)$%

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

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

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

$%\Rightarrow \exists x (x \in Hs) \rightarrow \exists x (x \in P \wedge x \ is \ sinful.)$%

$%\Leftrightarrow Hs \neq \varnothing \rightarrow \exists x (x \in P \wedge x \ is \ sinful.)$%

$%3. \ \begin {cases} \forall t_1 \forall t_2 (\{t_1, t_2\} \subseteq T \rightarrow (\neg(t_1 < t_2) \leftrightarrow t_1 \geq t_2)) \\ \exists t_s (t_s \in T \wedge \forall t (t \in T \rightarrow (t \geq t_s \leftrightarrow Hs \neq \varnothing))) \end {cases}$%

$%\Leftrightarrow \ \begin {cases} \forall t \forall t_s (t \in T \wedge t_s \in T \rightarrow (t < t_s \leftrightarrow \neg (t \geq t_s))) \\ \exists t_s (t_s \in T \wedge \forall t (t \in T \rightarrow (t \geq t_s \rightarrow Hs \neq \varnothing) \wedge (\neg (t \geq t_s) \rightarrow Hs = \varnothing))) \end {cases}$%

$%\Leftrightarrow \ \begin {cases} \forall t_s (t_s \in T \rightarrow \forall t (t \in T \rightarrow (t < t_s \leftrightarrow \neg (t \geq t_s)))) \\ \exists t_s (t_s \in T \wedge \forall t (t \in T \rightarrow (t \geq t_s \rightarrow Hs \neq \varnothing) \wedge (\neg (t \geq t_s) \rightarrow Hs = \varnothing))) \end {cases}$%

$%\Rightarrow \ \exists t_s (t_s \in T \wedge \begin {cases} \forall t (t \in T \rightarrow (t < t_s \leftrightarrow \neg (t \geq t_s))) \\ \forall t (t \in T \rightarrow (t \geq t_s \rightarrow Hs \neq \varnothing) \wedge (\neg (t \geq t_s) \rightarrow Hs = \varnothing)) \end {cases})$%

$%\Leftrightarrow \ \exists t_s (t_s \in T \wedge \forall t (t \in T \rightarrow \begin {cases} (t < t_s \leftrightarrow \neg (t \geq t_s) \\ (t \geq t_s \rightarrow Hs \neq \varnothing) \wedge (\neg (t \geq t_s) \rightarrow Hs = \varnothing) \end {cases}))$%

$%\Rightarrow \ \exists t_s (t_s \in T \wedge \forall t (t \in T \rightarrow (t \geq t_s \rightarrow Hs \neq \varnothing) \wedge (t < t_s \rightarrow Hs = \varnothing) ))$%