theorem :: RING_3:112

for p being Prime
for F being b₁ -characteristic Field
for E being Field st F includes E holds
E includes Z/ p