let u be non zero Element of (TOP-REAL 3); :: thesis: for P being Element of absolute st P = Dir u & u . 3 = 1 holds
|[(u . 1),(u . 2)]| in circle (0,0,1)
let P be Element of absolute ; :: thesis: ( P = Dir u & u . 3 = 1 implies |[(u . 1),(u . 2)]| in circle (0,0,1) )
assume that
A1: P = Dir u and
A2: u . 3 = 1 ; :: thesis: |[(u . 1),(u . 2)]| in circle (0,0,1)
P in conic (1,1,(- 1),0,0,0) ;
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) = 0 } by PASCAL:def 2;
then consider Q being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A3: P = Q and
A4: 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) = 0 ;
qfconic (1,1,(- 1),0,0,0,u) = 0 by A1, A3, A4;
then A5: ((((((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)) = 0 by PASCAL:def 1;
reconsider u1 = u . 1, u2 = u . 2 as Real ;
(u1 ^2) + (u2 ^2) = 1 by A2, A5;
hence |[(u . 1),(u . 2)]| in circle (0,0,1) by Th11; :: thesis: verum