theorem Th50: :: EC_PF_2:50

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 & Q `3_3 <> 0 holds
( ( P _EQ_ Q or P _EQ_ (compell_ProjCo (z,p)) . Q ) iff (P `1_3) * (Q `3_3) = (Q `1_3) * (P `3_3) )