let u be non zero Element of (TOP-REAL 3); :: thesis: ( ((u . 1) ^2) + ((u . 2) ^2) < 1 & u . 3 = 1 implies Dir u is Element of BK_model )
assume that
A1: ((u . 1) ^2) + ((u . 2) ^2) < 1 and
A2: u . 3 = 1 ; :: thesis: Dir u is Element of BK_model
reconsider P = Dir u as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;

now :: thesis: 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

let v be Element of (TOP-REAL 3); :: thesis: ( not v is zero & P = Dir v implies qfconic (1,1,(- 1),0,0,0,v) is negative )
assume that
A3: not v is zero and
A4: P = Dir v ; :: thesis: qfconic (1,1,(- 1),0,0,0,v) is negative
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)) + (- 1) by A2 ;
then qfconic (1,1,(- 1),0,0,0,u) < 1 + (- 1) by A1, XREAL_1:8;
hence qfconic (1,1,(- 1),0,0,0,v) is negative by A3, A4, BKMODEL1:81; :: thesis: verum

end;

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 Dir u is Element of BK_model by BKMODEL2:def 1; :: thesis: verum