:: deftheorem defines negative_conic BKMODEL1:def 6 :
for a, b, c, d, e, f being Real holds negative_conic (a,b,c,d,e,f) = { 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 } ;