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;then F is Subring of E by Def1;

hence F is Subfield of E by RING_3:45; :: thesis: verum

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

hence
( E is FieldExtension of F iff F is Subfield of E )
by A1; :: thesis: verumassume
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;then F is Subring of E by RING_3:43;

hence E is FieldExtension of F by Def1; :: thesis: verum