Let x0 of type ι be given.
Apply unknownprop_44069e352f5036a86127073abddc29a0ac5cf4eb6f4d81d6ec3a0209c2755103 with
x0,
∃ x1 . and (x1 ∈ SNoS_ omega) (SNoLt x0 x1) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply dneg with
∃ x1 . and (x1 ∈ SNoS_ omega) (SNoLt x0 x1).
Apply H3.
Apply Empty_eq with
SNoR_omega x0.
Let x1 of type ι be given.
Apply SepE with
SNoS_ omega,
λ x2 . SNoLt x0 x2,
x1,
False leaving 2 subgoals.
The subproof is completed by applying H7.
Apply H6.
Let x2 of type ο be given.
Apply H10 with
x1.
Apply andI with
x1 ∈ SNoS_ omega,
SNoLt x0 x1 leaving 2 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H9.