A1: now :: thesis:

let x be object ; :: thesis:
assume x in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ; :: thesis:
then ex P being Element of ProjCo (GF p) st
( x = P & (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) ) ;
hence x in ProjCo (GF p) ; :: thesis:

end;

reconsider D0 = [0,1,0] as Element of ProjCo (GF p) by Lm5;
(EC_WEqProjCo (a,b,p)) . D0 = 0. (GF p) by Lm5;
then D0 in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ;
hence { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } is non empty Subset of (ProjCo (GF p)) by A1, TARSKI:def 3; :: thesis: