Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Assume H0: ∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H2: x3 ∈ x0.
Let x5 of type ι → ι be given.
Let x6 of type ι be given.
Apply SepE with
setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3)),
λ x7 . equip (binintersect (DirGraphOutNeighbors x0 x1 x7) (DirGraphOutNeighbors x0 x1 x3)) x2,
x6,
∃ x7 . and (x7 ∈ setminus (DirGraphOutNeighbors x0 x1 x4) (Sing x3)) (x1 x6 x7) leaving 2 subgoals.
The subproof is completed by applying H6.
Apply setminusE with
x0,
binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3),
x6,
∃ x7 . and (x7 ∈ setminus (DirGraphOutNeighbors x0 x1 x4) (Sing x3)) (x1 x6 x7) leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H9: x6 ∈ x0.
Apply binintersectE with
DirGraphOutNeighbors x0 x1 x6,
DirGraphOutNeighbors x0 x1 x4,
x5 x6,
∃ x7 . and (x7 ∈ setminus (DirGraphOutNeighbors x0 x1 x4) (Sing x3)) (x1 x6 x7) leaving 2 subgoals.
Apply H5 with
x6.
Apply setminusI with
x0,
binunion (DirGraphOutNeighbors x0 x1 x4) (Sing x4),
x6 leaving 2 subgoals.
The subproof is completed by applying H9.
Apply binunionE with
DirGraphOutNeighbors x0 x1 x4,
Sing x4,
x6,
False leaving 3 subgoals.
The subproof is completed by applying H11.
Apply SepE2 with
x0,
λ x7 . and (x4 = x7 ⟶ ∀ x8 : ο . x8) (x1 x4 x7),
...,
... leaving 2 subgoals.