Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Assume H0: ∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2.
Assume H1:
∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4).
Let x2 of type ι be given.
Assume H3:
∀ x3 . x3 ⊆ x0 ⟶ atleastp (ordsucc x2) x3 ⟶ not (∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ not (x1 x4 x5)).
Let x3 of type ι be given.
Assume H4: x3 ∈ x0.
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with
x2,
DirGraphOutNeighbors x0 x1 x3,
atleastp (DirGraphOutNeighbors x0 x1 x3) x2 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H5.
Apply FalseE with
atleastp (DirGraphOutNeighbors x0 x1 x3) x2.
Apply H3 with
DirGraphOutNeighbors x0 x1 x3 leaving 3 subgoals.
The subproof is completed by applying Sep_Subq with
x0,
λ x4 . and (x3 = x4 ⟶ ∀ x5 : ο . x5) (x1 x3 x4).
The subproof is completed by applying H5.
Apply unknownprop_e153145abdef8d76c5a6e74702cb9d7f11b028f942da54501a84e1d9c7529c05 with
x0,
x1,
x3 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H4.