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.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Assume H3: x2 ⊆ x0.
Assume H4: x3 ⊆ x0.
Assume H5: x4 ⊆ x0.
Assume H6: x5 ⊆ x0.
Assume H7:
∀ x6 . x6 ∈ x4 ⟶ nIn x6 x2.
Assume H8:
∀ x6 . x6 ∈ x4 ⟶ nIn x6 x3.
Assume H9:
∀ x6 . x6 ∈ x4 ⟶ nIn x6 x5.
Assume H10:
∀ x6 . x6 ∈ x2 ⟶ nIn x6 x3.
Assume H11:
∀ x6 . x6 ∈ x2 ⟶ nIn x6 x5.
Assume H12:
∀ x6 . x6 ∈ x3 ⟶ nIn x6 x5.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Let x9 of type ι be given.
Let x10 of type ι be given.
Let x11 of type ι be given.
Let x12 of type ι be given.
Let x13 of type ι be given.
Let x14 of type ι be given.
Let x15 of type ι be given.
Assume H13: x6 ∈ x4.
Assume H14: x7 ∈ x4.
Assume H16: x14 ∈ x2.
Assume H17: x15 ∈ x5.
Assume H18: x6 = x7 ⟶ ∀ x16 : ο . x16.
Assume H19: x1 x6 x7.
Assume H20: x1 x6 x10.
Assume H21: x1 x6 x15.
Assume H22: x1 x7 x14.
Assume H23: x1 x7 x11.
Assume H24: x1 x12 x15.
Assume H25:
not (x1 x14 x6).
Assume H26: x1 x14 x15.
Assume H27: x1 x13 x15.
Apply H15 with
λ x16 x17 . ∀ x18 . x18 ∈ x17 ⟶ not (x1 x14 x18).
Apply unknownprop_cb75c47bae3a116273752c6fc8e52c777498313f2b5b4ef43d3ceb63348e2717 with
x10,
x11,
x12,
x13,
λ x16 . not (x1 x14 x16) leaving 4 subgoals.
Assume H36: x1 x14 x10.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with
u2 leaving 2 subgoals.
The subproof is completed by applying nat_2.
Apply atleastp_tra with
u3,
binintersect (DirGraphOutNeighbors x0 x1 x14) (DirGraphOutNeighbors x0 x1 x6),
u2 leaving 2 subgoals.
Apply atleastp_tra with
u3,
SetAdjoin (UPair x7 x10) x15,
binintersect (DirGraphOutNeighbors x0 x1 x14) (DirGraphOutNeighbors x0 x1 x6) leaving 2 subgoals.
Apply unknownprop_8a21f6cb5fc1714044127ec01eb34af4a43c7190a9ab55c5830d9c24f7e274f6 with
SetAdjoin (UPair x7 x10) x15,
x7,
x10,
x15 leaving 6 subgoals.
The subproof is completed by applying unknownprop_2f981bb386e15ae80933d34ec7d4feaabeedc598a3b07fb73b422d0a88302c67 with x7, x10, x15.
The subproof is completed by applying unknownprop_91640ab91f642c55f5e5a7feb12af7896a6f3419531543b011f7b54a888153d1 with x7, x10, x15.
The subproof is completed by applying unknownprop_ca66642b4e7ed479322d8970220318ddbb0c129adc66c35d9ce66f8223608389 with x7, x10, x15.
Assume H37: x7 = x10.
Apply H8 with
x7 leaving 2 subgoals.
The subproof is completed by applying H14.
Apply H37 with
λ x16 x17 . x17 ∈ x3.
The subproof is completed by applying L30.
Assume H37: x7 = x15.
Apply H9 with
x7 leaving 2 subgoals.
The subproof is completed by applying H14.
Apply H37 with
λ x16 x17 . x17 ∈ ....