theorem Th36: :: EC_PF_2:36

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds
( rep_pt P _EQ_ P & rep_pt P in EC_SetProjCo ((z `1),(z `2),p) )