:: deftheorem defines prime EC_PF_1:def 2 :
for IT being Field holds
( IT is prime iff for K1 being Field st K1 is strict Subfield of IT holds
K1 = IT );