theorem str1a: :: FIELD_7:8

for F being Field
for E being FieldExtension of F holds
( deg (E,F) = 1 iff E == F )