now :: thesis: for K1 being strict Subfield of F_Rat holds K1 = F_Rat

let K1 be strict Subfield of F_Rat ; :: thesis: K1 = F_Rat
set C1 = the carrier of K1;
A1: for x being set st x in F_Rat holds
x in K1 by Th25;
F_Rat is strict Subfield of F_Rat by EC_PF_1:1;
then F_Rat is strict Subfield of K1 by A1, EC_PF_1:7;
hence K1 = F_Rat by EC_PF_1:4; :: thesis: verum

end;

then for K1 being Field st K1 is strict Subfield of F_Rat holds
K1 = F_Rat ;
hence F_Rat is prime by EC_PF_1:def 2; :: thesis: verum