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 holds
( ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 ) iff ( P = Q or P = (compell_ProjCo (z,p)) . Q ) )