let E be Field; :: thesis: for R being Subring of E holds

( R is Subfield of E iff R is Field )

let R be Subring of E; :: thesis: ( R is Subfield of E iff R is Field )

( R is Subfield of E iff R is Field )

let R be Subring of E; :: thesis: ( R is Subfield of E iff R is Field )

now :: thesis: ( R is Field implies R is Subfield of E )

hence
( R is Subfield of E iff R is Field )
; :: thesis: verumassume B:
R is Field
; :: thesis: R is Subfield of E

( the carrier of R c= the carrier of E & the addF of R = the addF of E || the carrier of R & the multF of R = the multF of E || the carrier of R & 1. R = 1. E & 0. R = 0. E ) by C0SP1:def 3;

hence R is Subfield of E by EC_PF_1:def 1, B; :: thesis: verum

end;( the carrier of R c= the carrier of E & the addF of R = the addF of E || the carrier of R & the multF of R = the multF of E || the carrier of R & 1. R = 1. E & 0. R = 0. E ) by C0SP1:def 3;

hence R is Subfield of E by EC_PF_1:def 1, B; :: thesis: verum