theorem :: FIELD_5:15
for F being Field
for E being FieldExtension of F
for K being b2 -extending FieldExtension of F holds
( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )