let E be Field; :: thesis: for F being Subfield of E holds PrimeField F = PrimeField E
let F be Subfield of E; :: thesis: PrimeField F = PrimeField E
PrimeField F is Subfield of E by EC_PF_1:5;
then PrimeField E is Subfield of PrimeField F by Th92;
hence PrimeField F = PrimeField E by Th91; :: thesis: verum