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