Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: RealsStruct x0. Apply Field_is_CRing_with_id with Field_of_RealsStruct x0. Apply Field_Field_of_RealsStruct with x0. The subproof is completed by applying H0. ■