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