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;

qfconic (1,1,(- 1),0,0,0,u) is negative } ;

hence Dir u is Element of BK_model by BKMODEL2:def 1; :: thesis: verum

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

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,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;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

qfconic (1,1,(- 1),0,0,0,u) is negative } ;

hence Dir u is Element of BK_model by BKMODEL2:def 1; :: thesis: verum