let K1 be strict Subfield of F_Rat ; :: thesis: K1 = F_Rat
F_Rat is Subfield of F_Rat by EC_PF_1:1;
hence K1 = F_Rat by EC_PF_1:8, Th25; :: thesis: verum