theorem Th43: :: EC_PF_1:43

for p being Prime
for a, b, X, Y being Element of (GF p) holds
( Y |^ 2 = ((X |^ 3) + (a * X)) + b iff [X,Y,1] is Element of EC_SetProjCo (a,b,p) )