Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: RealsStruct x0. Apply Field_of_RealsStruct_3 with x0, λ x1 x2 . ∀ x3 . Field_div (Field_of_RealsStruct x0) x3 x1 = 0. Apply Field_div_undef3 with Field_of_RealsStruct x0. Apply Field_Field_of_RealsStruct with x0. The subproof is completed by applying H0. ■