theorem :: RING_3:96

for F being Field holds
( F is prime iff F = PrimeField F ) by EC_PF_1:def 2;