A1: now :: thesis: for x being object st x in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } holds
x in ProjCo (GF p)

let x be object ; :: thesis: ( x in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } implies x in ProjCo (GF p) )
assume x in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ; :: thesis: x in ProjCo (GF p)
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: verum

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: verum