reconsider u = |[0,0,1]| as non zero Element of (TOP-REAL 3) by ANPROJ_9:10;
reconsider P = Dir u as Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
qfconic (1,1,(- 1),0,0,0,u) is negative

proof

qfconic (1,1,(- 1),0,0,0,u) = ((((((1 * (u . 1)) * (u . 1)) + ((1 * (u . 2)) * (u . 2))) + (((- 1) * (u . 3)) * (u . 3))) + ((0 * (u . 1)) * (u . 2))) + ((0 * (u . 1)) * (u . 3))) + ((0 * (u . 2)) * (u . 3)) by PASCAL:def 1
.= - 1 ;
hence qfconic (1,1,(- 1),0,0,0,u) is negative ; :: thesis: verum

end;

then for v being Element of (TOP-REAL 3) st not v is zero & P = Dir v holds
qfconic (1,1,(- 1),0,0,0,v) is negative by BKMODEL1:81;
then P 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 (1,1,(- 1),0,0,0,u) is negative } ;
hence negative_conic (1,1,(- 1),0,0,0) is non empty Subset of (ProjectiveSpace (TOP-REAL 3)) ; :: thesis: verum