let p be Prime; for a, b being Element of (GF p) holds [0,1,0] is Element of EC_SetProjCo (a,b,p)
let a, b be Element of (GF p); [0,1,0] is Element of EC_SetProjCo (a,b,p)
( [0,1,0] is Element of ProjCo (GF p) & (EC_WEqProjCo (a,b,p)) . [0,1,0] = 0. (GF p) )
by Lm5;
then
[0,1,0] in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) }
;
hence
[0,1,0] is Element of EC_SetProjCo (a,b,p)
; verum