let F be Field; :: thesis: F is FieldExtension of F
F is Subring of F by Th1;
hence F is FieldExtension of F by Def1; :: thesis: verum