theorem :: FIELD_5:15

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F holds
( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )