Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: RealsStruct x0. Let x1 of type ι be given. Assume H1: x1 ∈ field0 x0. Let x2 of type ι be given. Assume H2: x2 ∈ field0 x0. Assume H3: RealsStruct_lt x0 x1 x2. Apply H3 with RealsStruct_leq x0 x1 x2. Assume H4: RealsStruct_leq x0 x1 x2. Assume H5: x1 = x2 ⟶ ∀ x3 : ο . x3. The subproof is completed by applying H4. ■