Let x0 of type ι be given.
Apply Field_of_RealsStruct_0 with
x0,
λ x1 x2 . ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ omega ⟶ 4a41c.. (Field_of_RealsStruct x0) x3 x4 ∈ x1.
Apply unknownprop_b75e15b7618f186de797a9c3b946547093a25c925a7003e20116b4ad0756b295 with
Field_of_RealsStruct x0.
Apply Field_of_RealsStruct_is_CRing_with_id with
x0.
The subproof is completed by applying H0.