theorem :: EC_PF_3:11

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 rep_pt P _EQ_ rep_pt Q holds
rep_pt P = rep_pt Q