for F, E being Field holds
( E is FieldExtension of F iff F is Subfield of E )