Let x0 of type ι be given.
Apply Field_of_RealsStruct_3 with
x0,
λ x1 x2 . ∀ x3 . a4228.. (Field_of_RealsStruct x0) x3 x1 = 0.
Apply unknownprop_4f3b2a0a51143dce17717ed5ce38a9c9525ab09c2359fb3f90194462ea08125a with
Field_of_RealsStruct x0.
Apply Field_Field_of_RealsStruct with
x0.
The subproof is completed by applying H0.