let E be Field; :: thesis: for F being strict Subfield of E holds E includes F
let F be strict Subfield of E; :: thesis: E includes F
( the carrier of F c= the carrier of E & the addF of F = the addF of E || the carrier of F & the multF of F = the multF of E || the carrier of F & 1. E = 1. F & 0. E = 0. F ) by EC_PF_1:def 1;
then F is strict Subring of E by C0SP1:def 3;
then ex T being strict Subring of E st T,F are_isomorphic ;
hence E includes F ; :: thesis: verum