:: deftheorem defines R_EllCur EC_PF_1:def 12 :
for p being Prime
for a, b being Element of (GF p) holds R_EllCur (a,b,p) = (R_ProjCo p) /\ (nabla (EC_SetProjCo (a,b,p)));