theorem Th4: :: FIELD_4:7

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