set a = z `1 ;
set b = z `2 ;

A1: now :: thesis: for x being object st x in { P where P is Element of EC_SetProjCo ((z `1),(z `2),p) : ( P `3_3 = 1 or P = [0,1,0] ) } holds
x in EC_SetProjCo ((z `1),(z `2),p)

let x be object ; :: thesis: ( x in { P where P is Element of EC_SetProjCo ((z `1),(z `2),p) : ( P `3_3 = 1 or P = [0,1,0] ) } implies x in EC_SetProjCo ((z `1),(z `2),p) )
assume x in { P where P is Element of EC_SetProjCo ((z `1),(z `2),p) : ( P `3_3 = 1 or P = [0,1,0] ) } ; :: thesis: x in EC_SetProjCo ((z `1),(z `2),p)
then ex P being Element of EC_SetProjCo ((z `1),(z `2),p) st
( x = P & ( P `3_3 = 1 or P = [0,1,0] ) ) ;
hence x in EC_SetProjCo ((z `1),(z `2),p) ; :: thesis: verum

end;

reconsider O = [0,1,0] as Element of EC_SetProjCo ((z `1),(z `2),p) by EC_PF_1:42;
O in { P where P is Element of EC_SetProjCo ((z `1),(z `2),p) : ( P `3_3 = 1 or P = [0,1,0] ) } ;
hence { P where P is Element of EC_SetProjCo ((z `1),(z `2),p) : ( P `3_3 = 1 or P = [0,1,0] ) } is non empty Subset of (EC_SetProjCo ((z `1),(z `2),p)) by A1, TARSKI:def 3; :: thesis: verum