let u be non zero Element of (TOP-REAL 3); ( ((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
; Dir u is Element of BK_model
reconsider P = Dir u as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
now 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);
( 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
;
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;
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; verum