set a = z `1 ;
set b = z `2 ;
A1:
now 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 ;
( 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] ) }
;
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)
;
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; verum