Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0:
∀ x2 . x2 ∈ x0 ⟶ SNo x2.
Apply Repl_invol_eq with
SNo,
minus_SNo,
x0,
λ x2 x3 . SNo_min_of x2 (minus_SNo x1) leaving 3 subgoals.
The subproof is completed by applying minus_SNo_invol.
The subproof is completed by applying H0.
Apply minus_SNo_max_min with
{minus_SNo x2|x2 ∈ x0},
x1 leaving 2 subgoals.
Let x2 of type ι be given.
Apply ReplE_impred with
x0,
λ x3 . minus_SNo x3,
x2,
SNo x2 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Assume H3: x3 ∈ x0.
Apply H4 with
λ x4 x5 . SNo x5.
Apply SNo_minus_SNo with
x3.
Apply H0 with
x3.
The subproof is completed by applying H3.
The subproof is completed by applying H1.