theorem Th47: :: EC_PF_1:47

for p being Prime
for a, b being Element of (GF p)
for P, Q being Element of ProjCo (GF p) st Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) holds
( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) )