theorem Th42: :: EC_PF_1:42

for p being Prime
for a, b being Element of (GF p) holds [0,1,0] is Element of EC_SetProjCo (a,b,p)