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