Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: RealsStruct x0.

Apply Field_of_RealsStruct_0 with x0, λ x1 x2 . ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ setminus x1 (Sing (field4 x0)) ⟶ Field_div (Field_of_RealsStruct x0) x3 x4 ∈ x1.

Apply Field_of_RealsStruct_3 with x0, λ x1 x2 . ∀ x3 . x3 ∈ ap (Field_of_RealsStruct x0) 0 ⟶ ∀ x4 . x4 ∈ setminus (ap (Field_of_RealsStruct x0) 0) (Sing x1) ⟶ Field_div (Field_of_RealsStruct x0) x3 x4 ∈ ap (Field_of_RealsStruct x0) 0.

Apply Field_div_clos with Field_of_RealsStruct x0.

Apply Field_Field_of_RealsStruct with x0.

The subproof is completed by applying H0.

■