let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p holds [0,1,0] is Element of EC_SetAffCo (z,p)
let z be Element of EC_WParam p; :: thesis: [0,1,0] is Element of EC_SetAffCo (z,p)
[0,1,0] is Element of EC_SetProjCo ((z `1),(z `2),p) by EC_PF_1:42;
then [0,1,0] in { P where P is Element of EC_SetProjCo ((z `1),(z `2),p) : ( P `3_3 = 1 or P = [0,1,0] ) } ;
hence [0,1,0] is Element of EC_SetAffCo (z,p) ; :: thesis: verum