theorem :: RING_3:109

for p being Prime
for F being strict Subfield of Z/ p holds F = Z/ p by EC_PF_1:def 2;