let F be 0 -characteristic Field; :: thesis: for E being Field st F includes E holds
E includes F_Rat
let E be Field; :: thesis: ( F includes E implies E includes F_Rat )
assume F includes E ; :: thesis: E includes F_Rat
then F is E -monomorphic by Th71;
then Char E = Char F by Th87
.= 0 by Def6 ;
then E is 0 -characteristic ;
hence E includes F_Rat by Th71; :: thesis: verum