let u be non zero Element of (); :: 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 () by ANPROJ_1:26;
now :: thesis: for v being Element of () st not v is zero & P = Dir v holds
qfconic (1,1,(- 1),0,0,0,v) is negative
let v be Element of (); :: 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 ;
hence qfconic (1,1,(- 1),0,0,0,v) is negative by ; :: thesis: verum
end;
then P in { P where P is Point of () : for u being Element of () 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