theorem :: RING_3:115

for F being strict Field holds
( F is prime iff ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) )