let u be non zero Element of (TOP-REAL 3); :: thesis: for P being Element of absolute st P = Dir u holds
u . 3 <> 0
let P be Element of absolute ; :: thesis: ( P = Dir u implies u . 3 <> 0 )
assume A1: P = Dir u ; :: thesis: u . 3 <> 0
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
A2: P = Q and
A3: 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 ;
A4: qfconic (1,1,(- 1),0,0,0,u) = 0 by A1, A2, A3;
thus u . 3 <> 0 :: thesis: verum
proof
assume A5: u . 3 = 0 ; :: thesis: contradiction
A6: ((((((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 A4, PASCAL:def 1;
reconsider u1 = u . 1, u2 = u . 2 as Real ;
(u1 ^2) + (u2 ^2) = 0 by A5, A6;
then ( u1 = 0 & u2 = 0 ) by COMPLEX1:1;
then ( u `1 = 0 & u `2 = 0 & u `3 = 0 ) by A5, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
hence contradiction by EUCLID_5:3, EUCLID_5:4; :: thesis: verum
end;