Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ο be given.
Apply PNoLtE with
SNoLev x0,
SNoLev x1,
λ x3 . x3 ∈ x0,
λ x3 . x3 ∈ x1,
x2 leaving 4 subgoals.
The subproof is completed by applying H2.
Apply PNoLt_E_ with
binintersect (SNoLev x0) (SNoLev x1),
λ x3 . x3 ∈ x0,
λ x3 . x3 ∈ x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H8.
Let x3 of type ι be given.
Assume H10:
PNoEq_ x3 (λ x4 . x4 ∈ x0) (λ x4 . x4 ∈ x1).
Assume H12: x3 ∈ x1.
Apply binintersectE with
SNoLev x0,
SNoLev x1,
x3,
x2 leaving 2 subgoals.
The subproof is completed by applying H9.
Apply SNoLev_prop with
PSNo x3 (λ x4 . x4 ∈ x0),
x2 leaving 2 subgoals.
The subproof is completed by applying L17.
Apply H3 with
PSNo x3 (λ x4 . x4 ∈ x0) leaving 8 subgoals.
The subproof is completed by applying L17.
Apply L20 with
λ x4 x5 . SNoEq_ x5 (PSNo x3 (λ x6 . x6 ∈ x0)) x0.
The subproof is completed by applying L21.
Apply L20 with
λ x4 x5 . SNoEq_ x5 (PSNo x3 (λ x6 . x6 ∈ x0)) x1.
The subproof is completed by applying L22.
Apply L20 with
λ x4 x5 . PNoLt (SNoLev x0) (λ x6 . x6 ∈ x0) x5 (λ x6 . x6 ∈ PSNo x3 (λ x7 . x7 ∈ x0)).
Apply PNoLtI3 with
SNoLev x0,
x3,
λ x4 . x4 ∈ x0,
λ x4 . x4 ∈ PSNo x3 (λ x5 . x5 ∈ x0) leaving 3 subgoals.
The subproof is completed by applying H13.
Apply PNoEq_sym_ with
x3,
λ x4 . ...,
....