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