set P = PrimeField F;
the carrier of (PrimeField F) = carrier/\ F by Def10;
then ( the carrier of (PrimeField F) is Subset of the carrier of F & the addF of (PrimeField F) = the addF of F || the carrier of (PrimeField F) & the multF of (PrimeField F) = the multF of F || the carrier of (PrimeField F) & 1. (PrimeField F) = 1. F & 0. (PrimeField F) = 0. F ) by Def10;
hence PrimeField F is strict Subfield of F by EC_PF_1:2; :: thesis: verum