let F be Field; :: thesis: for E being Subfield of F holds PrimeField F is Subfield of E
let E be Subfield of F; :: thesis: PrimeField F is Subfield of E
the carrier of (PrimeField F) c= the carrier of E

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (PrimeField F) or x in the carrier of E )
assume x in the carrier of (PrimeField F) ; :: thesis: x in the carrier of E
then x in carrier/\ F by Def10;
then ex y being Element of F st
( x = y & ( for K being Subfield of F holds y in K ) ) ;
then x in E ;
hence x in the carrier of E ; :: thesis: verum

end;

hence PrimeField F is Subfield of E by EC_PF_1:6; :: thesis: verum