theorem Th48: :: EC_PF_1:48

for p being Prime
for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 <> 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `3_3 = 1 )