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 } ;
then consider Q being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A1: P = Q and
A2: for u being Element of (TOP-REAL 3) st not u is zero & Q = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) is negative ;
consider u being Element of (TOP-REAL 3) such that
A3: not u is zero and
A4: P = Dir u by ANPROJ_1:26;
reconsider u1 = u . 1, u2 = u . 2, u3 = u . 3 as Real ;
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 . 2))) + ((0 * (u . 2)) * (u . 3)) by PASCAL:def 1
.= (((u . 1) ^2) + ((u . 2) ^2)) - ((u . 3) ^2) ;
then ((u1 ^2) + (u2 ^2)) - (u3 ^2) < 0 by A1, A3, A4, A2;
then A5: (((u1 ^2) + (u2 ^2)) - (u3 ^2)) + (u3 ^2) < 0 + (u3 ^2) by XREAL_1:6;
A6: u . 3 <> 0

proof

assume A7: u . 3 = 0 ; :: thesis: contradiction
A8: 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 . 2))) + ((0 * (u . 2)) * (u . 3)) by PASCAL:def 1
.= (u1 ^2) + (u2 ^2) by A7 ;
0 ^2 = 0 ;
then ( 0 <= u1 ^2 & 0 <= u2 ^2 ) by SQUARE_1:12;
hence contradiction by A1, A3, A4, A2, A8; :: thesis: verum

end;

reconsider k = 1 / (u3 ^2) as Real ;
0 < u3 ^2 by A6, SQUARE_1:12;
then A10: ((u1 ^2) + (u2 ^2)) * k < (u3 ^2) * k by A5, XREAL_1:68;
A11: ( (u1 ^2) * k = (u1 / u3) ^2 & (u2 ^2) * k = (u2 / u3) ^2 ) by BKMODEL1:12;
|[((u . 1) / (u . 3)),((u . 2) / (u . 3)),1]| <> 0. (TOP-REAL 3)

proof

assume |[((u . 1) / (u . 3)),((u . 2) / (u . 3)),1]| = 0. (TOP-REAL 3) ; :: thesis: contradiction
then 1 = |[0,0,0]| `3 by EUCLID_5:2, EUCLID_5:4;
hence contradiction by EUCLID_5:2; :: thesis: verum

end;

then not |[((u . 1) / (u . 3)),((u . 2) / (u . 3)),1]| is zero ;
then reconsider v = |[((u . 1) / (u . 3)),((u . 2) / (u . 3)),1]| as non zero Element of (TOP-REAL 3) ;
A14: ( (u . 3) * ((u . 1) / (u . 3)) = u . 1 & (u . 3) * ((u . 2) / (u . 3)) = u . 2 ) by A6, XCMPLX_1:87;
(u . 3) * v = |[((u . 3) * ((u . 1) / (u . 3))),((u . 3) * ((u . 2) / (u . 3))),((u . 3) * 1)]| by EUCLID_5:8
.= |[(u `1),(u . 2),(u . 3)]| by A14, EUCLID_5:def 1
.= |[(u `1),(u `2),(u . 3)]| by EUCLID_5:def 2
.= |[(u `1),(u `2),(u `3)]| by EUCLID_5:def 3
.= u by EUCLID_5:3 ;
then are_Prop v,u by A6, ANPROJ_1:1;
then A15: P = Dir v by A3, A4, ANPROJ_1:22;
|[(v . 1),(v . 2)]| in inside_of_circle (0,0,1)

proof

reconsider t = |[(v . 1),(v . 2)]| as Element of (TOP-REAL 2) ;
|.(t - |[0,0]|).| < 1

proof

A16: |.(t - |[0,0]|).| = |.|[((v . 1) - 0),((v . 2) - 0)]|.| by EUCLID:62
.= |.t.| ;
A17: ( v . 1 = t `1 & v . 2 = t `2 ) by EUCLID:52;
|.t.| ^2 = ((u1 ^2) * k) + ((u2 ^2) * k) by A17, JGRAPH_1:29, A11;
then |.t.| ^2 < 1 ^2 by A10, A6, XCMPLX_1:106;
hence |.(t - |[0,0]|).| < 1 by A16, SQUARE_1:48; :: thesis: verum

end;

hence |[(v . 1),(v . 2)]| in inside_of_circle (0,0,1) ; :: thesis: verum

end;

then reconsider w = |[(v . 1),(v . 2)]| as Element of inside_of_circle (0,0,1) ;
take w ; :: thesis: ex u being non zero Element of (TOP-REAL 3) st
( Dir u = P & u . 3 = 1 & w = |[(u . 1),(u . 2)]| )
v . 3 = v `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ;
hence ex u being non zero Element of (TOP-REAL 3) st
( Dir u = P & u . 3 = 1 & w = |[(u . 1),(u . 2)]| ) by A15; :: thesis: verum