theorem alg0: :: FIELD_7:31

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