let E be Subfield of F; :: thesis: E is finite
the carrier of E c= the carrier of F by EC_PF_1:def 1;
hence E is finite ; :: thesis: verum