let u be non zero Element of (TOP-REAL 3); :: thesis: for P being Point of (ProjectiveSpace (TOP-REAL 3)) st P = Dir u & u . 3 = 1 & |[(u . 1),(u . 2)]| in circle (0,0,1) holds
P is Element of absolute
let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( P = Dir u & u . 3 = 1 & |[(u . 1),(u . 2)]| in circle (0,0,1) implies P is Element of absolute )
assume that
A1: P = Dir u and
A2: u . 3 = 1 and
A3: |[(u . 1),(u . 2)]| in circle (0,0,1) ; :: thesis: P is Element of absolute
reconsider u1 = u . 1, u2 = u . 2, u3 = u . 3 as Real ;
A4: (u1 ^2) + (u2 ^2) = |.|[(u1 - 0),(u2 - 0)]|.| ^2 by TOPGEN_5:9
.= |.(|[u1,u2]| - |[0,0]|).| ^2 by EUCLID:62
.= 1 ^2 by A3, TOPREAL9:43
.= 1 ;

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) = 0

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) = 0 )
assume that
A5: not v is zero and
A6: P = Dir v ; :: thesis: qfconic (1,1,(- 1),0,0,0,v) = 0
are_Prop u,v by A1, A5, A6, ANPROJ_1:22;
then consider a being Real such that
A7: a <> 0 and
A8: u = a * v by ANPROJ_1:1;
reconsider v1 = v . 1, v2 = v . 2, v3 = v . 3 as Real ;
( u1 = a * v1 & u2 = a * v2 & u3 = a * v3 ) by A8, RVSUM_1:44;
then A9: ( v1 = u1 / a & v2 = u2 / a & v3 = u3 / a ) by A7, XCMPLX_1:89;
qfconic (1,1,(- 1),0,0,0,v) = ((((((1 * v1) * v1) + ((1 * v2) * v2)) + (((- 1) * v3) * v3)) + ((0 * v1) * v2)) + ((0 * v1) * v3)) + ((0 * v2) * v3) by PASCAL:def 1
.= (((u1 / a) * (u1 / a)) + ((u2 / a) * (u2 / a))) - ((u3 / a) * (u3 / a)) by A9
.= ((((1 / a) * u1) * (u1 / a)) + ((u2 / a) * (u2 / a))) - ((u3 / a) * (u3 / a)) by XCMPLX_1:99
.= ((((1 / a) * u1) * ((1 / a) * u1)) + ((u2 / a) * (u2 / a))) - ((u3 / a) * (u3 / a)) by XCMPLX_1:99
.= (((((1 / a) * (1 / a)) * u1) * u1) + (((1 / a) * u2) * (u2 / a))) - ((u3 / a) * (u3 / a)) by XCMPLX_1:99
.= (((((1 / a) * (1 / a)) * u1) * u1) + (((1 / a) * u2) * ((1 / a) * u2))) - ((u3 / a) * (u3 / a)) by XCMPLX_1:99
.= (((((1 / a) * (1 / a)) * u1) * u1) + ((((1 / a) * (1 / a)) * u2) * u2)) - (((1 / a) * u3) * (u3 / a)) by XCMPLX_1:99
.= (((((1 / a) * (1 / a)) * u1) * u1) + ((((1 / a) * (1 / a)) * u2) * u2)) - (((1 / a) * u3) * ((1 / a) * u3)) by XCMPLX_1:99
.= ((1 / a) * (1 / a)) * (((u1 ^2) + (u2 * u2)) - (u3 * u3))
.= 0 by A2, A4 ;
hence qfconic (1,1,(- 1),0,0,0,v) = 0 ; :: thesis: 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) = 0 } ;
hence P is Element of absolute by PASCAL:def 2; :: thesis: verum