let F be Field; :: thesis: for x being Element of (PrimeField F) holds x is Element of F
let x be Element of (PrimeField F); :: thesis: x is Element of F
A1: the carrier of (PrimeField F) = carrier/\ F by Def10;
x in the carrier of (PrimeField F) ;
hence x is Element of F by A1; :: thesis: verum