Let x0 of type ι → ι → ο be given.
Assume H0: ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1.
Assume H1:
∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3).
Assume H2:
∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3)).
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply setminusE with
setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1)),
DirGraphOutNeighbors u18 x0 x2,
x3,
4b3fa.. x0 x1 x3 ∈ setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2) leaving 2 subgoals.
The subproof is completed by applying H5.
Apply binintersectE with
DirGraphOutNeighbors u18 x0 x3,
DirGraphOutNeighbors u18 x0 x1,
4b3fa.. x0 x1 x3,
4b3fa.. x0 x1 x3 ∈ setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2) leaving 2 subgoals.
Apply unknownprop_dcbea086d2a993ee188398118e0404b9efebe2800da06715fdb8a87532c8d892 with
x0,
x1,
x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
Apply setminusI with
DirGraphOutNeighbors u18 x0 x1,
Sing x2,
4b3fa.. x0 x1 x3 leaving 2 subgoals.
The subproof is completed by applying H9.
Apply H7.
Apply unknownprop_426b271b8453605fe796f284fb15405fbff198d07b0c3dc7b8c218dee82a5c65 with
u18,
x0,
x3,
x2 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply SingE with
x2,
4b3fa.. x0 x1 x3,
λ x4 x5 . x4 ∈ DirGraphOutNeighbors u18 x0 x3 leaving 2 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying H8.