set C = { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) is negative } ;
{ P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) is negative } c= the carrier of (ProjectiveSpace (TOP-REAL 3))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) is negative } or x in the carrier of (ProjectiveSpace (TOP-REAL 3)) )
assume x in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) is negative } ; :: thesis: x in the carrier of (ProjectiveSpace (TOP-REAL 3))
then ex P being Point of (ProjectiveSpace (TOP-REAL 3)) st
( x = P & ( for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) is negative ) ) ;
hence x in the carrier of (ProjectiveSpace (TOP-REAL 3)) ; :: thesis: verum

end;

hence { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) is negative } is Subset of (ProjectiveSpace (TOP-REAL 3)) ; :: thesis: verum