for K being Field st K is strict Subfield of PrimeField F holds
K = PrimeField F by Th91;
hence PrimeField F is prime by EC_PF_1:def 2; :: thesis: verum