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