:: deftheorem defines R_ProjCo EC_PF_1:def 11 :
for p being Prime holds R_ProjCo p = { [P,Q] where P, Q is Element of ProjCo (GF p) : P _EQ_ Q } ;