let F be Field; :: thesis: for R being Subring of F holds
( R is Subfield of F iff R is Field )
let R be Subring of F; :: thesis: ( R is Subfield of F iff R is Field )
( the carrier of R c= the carrier of F & the addF of R = the addF of F || the carrier of R & the multF of R = the multF of F || the carrier of R & 1. R = 1. F & 0. R = 0. F ) by C0SP1:def 3;
hence ( R is Subfield of F iff R is Field ) by EC_PF_1:def 1; :: thesis: verum