:: deftheorem defines EC_SetProjCo EC_PF_1:def 9 :
for p being Prime
for a, b being Element of (GF p) holds EC_SetProjCo (a,b,p) = { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ;