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 )

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

assume 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;

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