let F be Field; :: thesis: 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) ) )
let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F holds
( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )
let K be E -extending FieldExtension of F; :: thesis: ( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )
set VK = VecSp (K,F);
set VE = VecSp (E,F);

now :: thesis: ( K is F -finite implies ( E is F -finite & deg (E,F) <= deg (K,F) ) )

assume K is F -finite ; :: thesis: ( E is F -finite & deg (E,F) <= deg (K,F) )
then reconsider VK = VecSp (K,F) as finite-dimensional VectSp of F by FIELD_4:def 8;
A: deg (K,F) = dim VK by FIELD_4:def 7;
B: VecSp (E,F) is Subspace of VK by sp;
then C: dim (VecSp (E,F)) <= dim VK by VECTSP_9:25;
thus E is F -finite by B, FIELD_4:def 8; :: thesis: deg (E,F) <= deg (K,F)
thus deg (E,F) <= deg (K,F) by A, C, FIELD_4:def 7; :: thesis: verum

end;

hence ( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) ) ; :: thesis: verum