let F be Field; :: thesis: for E being strict Subfield of PrimeField F holds E = PrimeField F
let E be strict Subfield of PrimeField F; :: thesis: E = PrimeField F
set K = PrimeField F;
A1: ( the carrier of E c= the carrier of (PrimeField F) & the addF of E = the addF of (PrimeField F) || the carrier of E & the multF of E = the multF of (PrimeField F) || the carrier of E & 1. E = 1. (PrimeField F) & 0. E = 0. (PrimeField F) ) by EC_PF_1:def 1;
E is Subfield of F by EC_PF_1:5;
then carrier/\ F c= the carrier of E by Lm13;
then the carrier of E = the carrier of (PrimeField F) by EC_PF_1:def 1, Def10;
hence E = PrimeField F by A1; :: thesis: verum