let F, E be Field; :: thesis: ( E is FieldExtension of F iff F is Subfield of E )

A1: now :: thesis: ( E is FieldExtension of F implies F is Subfield of E )

assume E is FieldExtension of F ; :: thesis: F is Subfield of E
then F is Subring of E by Def1;
hence F is Subfield of E by RING_3:45; :: thesis: verum

end;

now :: thesis: ( F is Subfield of E implies E is FieldExtension of F )

assume F is Subfield of E ; :: thesis: E is FieldExtension of F
then F is Subring of E by RING_3:43;
hence E is FieldExtension of F by Def1; :: thesis: verum

end;

hence ( E is FieldExtension of F iff F is Subfield of E ) by A1; :: thesis: verum