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