let S be Subfield of F; :: thesis: S is p -characteristic
S is Subring of F by Lm1;
hence S is p -characteristic ; :: thesis: verum