| ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5 ⟶ ∀ x6 . x6 ⊆ x0 ⟶ x1 ∈ x6 ⟶ x2 ∈ x6 ⟶ (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ x3 x7 x8 ∈ x6) ⟶ (∀ x7 . x7 ∈ x6 ⟶ explicit_Field_minus x0 x1 x2 x3 x4 x7 ∈ x6) ⟶ (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ x4 x7 x8 ∈ x6) ⟶ (∀ x7 . x7 ∈ x6 ⟶ (x7 = x1 ⟶ ∀ x8 : ο . x8) ⟶ ∀ x8 : ο . (∀ x9 . and (x9 ∈ x6) (x4 x7 x9 = x2) ⟶ x8) ⟶ x8) ⟶ explicit_OrderedField x6 x1 x2 x3 x4 x5 |
|