theorem Th3: :: FIELD_4:6

for F being Field holds F is FieldExtension of F