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
per cases then ( (a ^2) + (b ^2) = 1 or (a ^2) + (b ^2) < 1 ) by XXREAL_0:1;
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;
now :: thesis: ( |[(u . 1),(u . 2)]| in circle (0,0,1) & u . 3 = 1 )
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;
then P is Element of absolute by BKMODEL1:86;
hence Dir |[a,b,1]| in BK_model \/ absolute by XBOOLE_0:def 3; :: thesis: verum
end;
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;
end;