We will prove (setprod R R = R ∧ Rlt (a1,a2) (b1,b2)) ∨ (setprod R R = rational_numbers ∧ Rlt (a1,a2) (b1,b2)) ∨ (setprod R R = ω ∧ (a1,a2) ∈ (b1,b2)) ∨ (setprod R R = ω ∖ {0} ∧ (a1,a2) ∈ (b1,b2)) ∨ (setprod R R = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ (a1,a2) = (i,m) ∧ (b1,b2) = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) ∨ (setprod R R = setprod R R ∧ ∃c1 c2 d1 d2 : set, (a1,a2) = (c1,c2) ∧ (b1,b2) = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2))) ∨ (ordinal (setprod R R) ∧ setprod R R ≠ R ∧ setprod R R ≠ rational_numbers ∧ setprod R R ≠ setprod 2 ω ∧ setprod R R ≠ setprod R R ∧ (a1,a2) ∈ (b1,b2)).

We will prove setprod R R = setprod R R ∧ ∃c1 c2 d1 d2 : set, (a1,a2) = (c1,c2) ∧ (b1,b2) = (d1,d2) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).

We use a1 to witness the existential quantifier.

We use a2 to witness the existential quantifier.

We use b1 to witness the existential quantifier.

We use b2 to witness the existential quantifier.

We will prove (a1,a2) = (a1,a2) ∧ (b1,b2) = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).

Apply andI to the current goal.

Use reflexivity.

An exact proof term for the current goal is Hdisj.