let P be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for u being non zero Element of (TOP-REAL 3) st P = Dir u & P in BK_model holds
u . 3 <> 0
let u be non zero Element of (TOP-REAL 3); :: thesis: ( P = Dir u & P in BK_model implies u . 3 <> 0 )
assume that
A1: P = Dir u and
A2: P in BK_model ; :: thesis: u . 3 <> 0
assume A3: u . 3 = 0 ; :: thesis: contradiction
consider Q being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A4: P = Q and
A5: 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 by A2;
A6: qfconic (1,1,(- 1),0,0,0,u) is negative by A1, A4, A5;
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
.= ((u . 1) ^2) + ((u . 2) ^2) by A3 ;
then ( u . 1 = 0 & u . 2 = 0 ) by A6, BKMODEL1:19;
then ( u `1 = 0 & u `2 = 0 & u `3 = 0 ) by A3, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
hence contradiction by EUCLID_5:3, EUCLID_5:4; :: thesis: verum