:: deftheorem defines EC_SetAffCo EC_PF_3:def 1 :
for p being 5 _or_greater Prime
for z being Element of EC_WParam p holds EC_SetAffCo (z,p) = { P where P is Element of EC_SetProjCo ((z `1),(z `2),p) : ( P `3_3 = 1 or P = [0,1,0] ) } ;