Proofgold Proof

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