Let x0 of type ι be given.

Assume H0: x0 ∈ u6.

Let x1 of type ι be given.

Assume H1: x1 ∈ u6.

Let x2 of type ι be given.

Assume H2: x2 ∈ u6.

Let x3 of type ι be given.

Assume H3: x3 ∈ u6.

Assume H4: not (TwoRamseyGraph_4_6_35_a x0 x1 x2 x3).

Claim L5: ordinal x0

Apply nat_p_ordinal with x0.

Apply nat_p_trans with u6, x0 leaving 2 subgoals.

The subproof is completed by applying nat_6.

The subproof is completed by applying H0.

Claim L6: ordinal x1

Apply nat_p_ordinal with x1.

Apply nat_p_trans with u6, x1 leaving 2 subgoals.

The subproof is completed by applying nat_6.

The subproof is completed by applying H1.

Claim L7: ordinal x2

Apply nat_p_ordinal with x2.

Apply nat_p_trans with u6, x2 leaving 2 subgoals.

The subproof is completed by applying nat_6.

The subproof is completed by applying H2.

Claim L8: ordinal x3

Apply nat_p_ordinal with x3.

Apply nat_p_trans with u6, x3 leaving 2 subgoals.

The subproof is completed by applying nat_6.

The subproof is completed by applying H3.

Apply ordinal_trichotomy_or_impred with x1, x3, or (In2_lexicographic x0 x1 x2 x3) (In2_lexicographic x2 x3 x0 x1) leaving 5 subgoals.

The subproof is completed by applying L6.

The subproof is completed by applying L8.

Assume H9: x1 ∈ x3.

Apply orIL with In2_lexicographic x0 x1 x2 x3, In2_lexicographic x2 x3 x0 x1.

Apply orIL with x1 ∈ x3, and (x1 = x3) (x0 ∈ x2).

The subproof is completed by applying H9.

Assume H9: x1 = x3.

Apply ordinal_trichotomy_or_impred with x0, x2, or (In2_lexicographic x0 x1 x2 x3) (In2_lexicographic x2 x3 x0 x1) leaving 5 subgoals.

The subproof is completed by applying L5.

The subproof is completed by applying L7.

Assume H10: x0 ∈ x2.

Apply orIL with In2_lexicographic x0 x1 x2 x3, In2_lexicographic x2 x3 x0 x1.

Apply orIR with x1 ∈ x3, and (x1 = x3) (x0 ∈ x2).

Apply andI with x1 = x3, x0 ∈ x2 leaving 2 subgoals.

The subproof is completed by applying H9.

The subproof is completed by applying H10.

Assume H10: x0 = x2.

Apply FalseE with or (In2_lexicographic x0 x1 x2 x3) (In2_lexicographic x2 x3 x0 x1).

Apply H4.

Apply H9 with λ x4 x5 . TwoRamseyGraph_4_6_35_a x0 x1 x2 x4.

Apply H10 with λ x4 x5 . TwoRamseyGraph_4_6_35_a x0 x1 x4 x1.

Apply unknownprop_c92c0588de1ba6f1a5352aaa897a2358c5ed2f086efe24dfed8c7d8036084229 with x0, x1 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Assume H10: x2 ∈ x0.

Apply orIR with In2_lexicographic x0 x1 x2 x3, In2_lexicographic x2 x3 x0 x1.

Apply orIR with x3 ∈ x1, and (x3 = x1) (x2 ∈ x0).

Apply andI with x3 = x1, x2 ∈ x0 leaving 2 subgoals.

Let x4 of type ι → ι → ο be given.

The subproof is completed by applying H9 with λ x5 x6 . x4 x6 x5.

The subproof is completed by applying H10.

Assume H9: x3 ∈ x1.

Apply orIR with In2_lexicographic x0 x1 x2 x3, In2_lexicographic x2 x3 x0 x1.

Apply orIL with x3 ∈ x1, and (x3 = x1) (x2 ∈ x0).

The subproof is completed by applying H9.

■

Proofgold Proof