let a, b be Real; :: thesis: ( (a ^2) + (b ^2) <= 1 implies Dir |[a,b,1]| in BK_model \/ absolute )

assume (a ^2) + (b ^2) <= 1 ; :: thesis: Dir |[a,b,1]| in BK_model \/ absolute

assume (a ^2) + (b ^2) <= 1 ; :: thesis: Dir |[a,b,1]| in BK_model \/ absolute

per cases then
( (a ^2) + (b ^2) = 1 or (a ^2) + (b ^2) < 1 )
by XXREAL_0:1;

end;

suppose A1:
(a ^2) + (b ^2) = 1
; :: thesis: Dir |[a,b,1]| in BK_model \/ absolute

reconsider u = |[a,b,1]| as non zero Element of (TOP-REAL 3) ;

reconsider P = Dir u as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;

hence Dir |[a,b,1]| in BK_model \/ absolute by XBOOLE_0:def 3; :: thesis: verum

end;reconsider P = Dir u as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;

now :: thesis: ( |[(u . 1),(u . 2)]| in circle (0,0,1) & u . 3 = 1 )

then
P is Element of absolute
by BKMODEL1:86;B1: u . 1 =
u `1
by EUCLID_5:def 1

.= a by EUCLID_5:2 ;

u . 2 = u `2 by EUCLID_5:def 2

.= b by EUCLID_5:2 ;

hence |[(u . 1),(u . 2)]| in circle (0,0,1) by A1, B1, BKMODEL1:13; :: thesis: u . 3 = 1

thus u . 3 = |[a,b,1]| `3 by EUCLID_5:def 3

.= 1 by EUCLID_5:2 ; :: thesis: verum

end;.= a by EUCLID_5:2 ;

u . 2 = u `2 by EUCLID_5:def 2

.= b by EUCLID_5:2 ;

hence |[(u . 1),(u . 2)]| in circle (0,0,1) by A1, B1, BKMODEL1:13; :: thesis: u . 3 = 1

thus u . 3 = |[a,b,1]| `3 by EUCLID_5:def 3

.= 1 by EUCLID_5:2 ; :: thesis: verum

hence Dir |[a,b,1]| in BK_model \/ absolute by XBOOLE_0:def 3; :: thesis: verum

suppose A2:
(a ^2) + (b ^2) < 1
; :: thesis: Dir |[a,b,1]| in BK_model \/ absolute

reconsider w = |[a,b,1]| as non zero Element of (TOP-REAL 3) ;

( w `1 = a & w `2 = b & w `3 = 1 ) by EUCLID_5:2;

then ( w . 1 = a & w . 2 = b & w . 3 = 1 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

then Dir |[a,b,1]| is Element of BK_model by A2, Th27;

hence Dir |[a,b,1]| in BK_model \/ absolute by XBOOLE_0:def 3; :: thesis: verum

end;( w `1 = a & w `2 = b & w `3 = 1 ) by EUCLID_5:2;

then ( w . 1 = a & w . 2 = b & w . 3 = 1 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

then Dir |[a,b,1]| is Element of BK_model by A2, Th27;

hence Dir |[a,b,1]| in BK_model \/ absolute by XBOOLE_0:def 3; :: thesis: verum