reconsider u = |[0,0,1]| as non zero Element of (TOP-REAL 3) by ANPROJ_9:10;
( u `1 = 0 & u `2 = 0 & u `3 = 1 )
by EUCLID_5:2;
then A1:
( u . 1 = 0 & u . 2 = 0 & u . 3 = 1 )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
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
by A1
;
hence
qfconic (1,1,
(- 1),
0,
0,
0,
u) is
negative
;
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))
; verum