Let I, S, m1 and m2 be given.

Assume _HordI: ordinal I.

Assume _HSsubI: S ⊆ I.

Assume Hm1S: m1 ∈ S.

Assume Hm1least: ∀s : set, s ∈ S → m1 ⊆ s.

Assume Hm2S: m2 ∈ S.

Assume Hm2least: ∀s : set, s ∈ S → m2 ⊆ s.

Apply set_ext to the current goal.

An exact proof term for the current goal is (Hm1least m2 Hm2S).

An exact proof term for the current goal is (Hm2least m1 Hm1S).

∎