for p being Prime
for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) holds
( P is_on_curve EC_WEqProjCo (a,b,p) iff P is Element of EC_SetProjCo (a,b,p) )