Proofgold Proof

Apply explicit_OrderedField_E with x0, x1, x2, x3, x4, x5, x6 ⊆ x0 ⟶ explicit_Field x6 x1 x2 x3 x4 ⟶ ∀ x7 : ο . ((∀ x8 . x8 ∈ x6 ⟶ explicit_Field_minus x6 x1 x2 x3 x4 x8 = explicit_Field_minus x0 x1 x2 x3 x4 x8) ⟶ (∀ x8 . x8 ∈ x6 ⟶ explicit_Field_minus x0 x1 x2 x3 x4 x8 ∈ x6) ⟶ {x8 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x8} = {x8 ∈ x6|natOfOrderedField_p x6 x1 x2 x3 x4 x5 x8} ⟶ {x8 ∈ {x8 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x8}|x8 = x1 ⟶ ∀ x9 : ο . x9} = {x8 ∈ {x8 ∈ x6|natOfOrderedField_p x6 x1 x2 x3 x4 x5 x8}|x8 = x1 ⟶ ∀ x9 : ο . x9} ⟶ {x8 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x8 ∈ {x9 ∈ {x9 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x9}|x9 = x1 ⟶ ∀ x10 : ο . x10}) (x8 = x1)) (x8 ∈ {x9 ∈ {x9 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x9}|x9 = x1 ⟶ ∀ x10 : ο . x10})} = {x8 ∈ x6|or (or (explicit_Field_minus x6 x1 x2 x3 x4 x8 ∈ {x9 ∈ {x9 ∈ x6|natOfOrderedField_p x6 x1 x2 x3 x4 x5 x9}|x9 = x1 ⟶ ∀ x10 : ο . x10}) (x8 = x1)) (x8 ∈ {x9 ∈ {x9 ∈ x6|natOfOrderedField_p x6 x1 x2 x3 x4 x5 x9}|x9 = x1 ⟶ ∀ x10 : ο . x10})} ⟶ {x8 ∈ x0|explicit_OrderedField_rationalp x0 x1 x2 x3 x4 x5 x8} = {x8 ∈ x6|explicit_OrderedField_rationalp x6 x1 x2 x3 x4 x5 x8} ⟶ x7) ⟶ x7.