let P, PP1, PP2 be Element of real_projective_plane; :: thesis:
let P1, P2 be Element of absolute ; :: thesis:
let Q be Element of real_projective_plane; :: thesis:
assume that
A1: P1 <> P2 and
A2: PP1 = P1 and
A3: PP2 = P2 and
A4: P in BK_model and
A5: P,PP1,PP2 are_collinear and
A6: Q in tangent P1 and
A7: Q in tangent P2 ; :: thesis:
A8: P <> Q

assume P = Q ; :: thesis:
then BK_model meets tangent P1 by A4, A6, XBOOLE_0:def 4;
hence contradiction by Th30; :: thesis:

end;

consider u being Element of (TOP-REAL 3) such that
A9: not u is zero and
A10: Dir u = Q by ANPROJ_1:26;

per cases ;

suppose A11: u `3 <> 0 ; :: thesis:

reconsider v = |[((u `1) / (u `3)),((u `2) / (u `3)),1]| as non zero Element of (TOP-REAL 3) by BKMODEL1:41;
A13: ( (u `3) * ((u `1) / (u `3)) = u `1 & (u `3) * ((u `2) / (u `3)) = u `2 ) by A11, XCMPLX_1:87;
(u `3) * v = |[((u `3) * ((u `1) / (u `3))),((u `3) * ((u `2) / (u `3))),((u `3) * 1)]| by EUCLID_5:8
.= u by A13, EUCLID_5:3 ;
then are_Prop v,u by A11, ANPROJ_1:1;
then A14: ( Dir v = Q & v . 3 = 1 ) by A10, A9, ANPROJ_1:22;
reconsider PP = P as Element of BK_model by A4;
reconsider QQ = Q as Element of (ProjectiveSpace (TOP-REAL 3)) ;
consider R being Element of absolute such that
A15: PP,QQ,R are_collinear by A8, A14, Th03;
reconsider R = R as Element of real_projective_plane ;
take R ; :: thesis:
thus ( R in absolute & P,Q,R are_collinear ) by A15; :: thesis:

end;

suppose u `3 = 0 ; :: thesis:

then A16: u . 3 = 0 by EUCLID_5:def 3;
then ( Q = pole_infty P1 & Q = pole_infty P2 ) by A6, A7, A9, A10, Th28;
then consider up being non zero Element of (TOP-REAL 3) such that
A17: P1 = Dir up and
A18: P2 = Dir |[(- (up `1)),(- (up `2)),1]| and
A19: up `3 = 1 by A1, Th20;
consider up1 being non zero Element of (TOP-REAL 3) such that
A20: ((up1 . 1) ^2) + ((up1 . 2) ^2) = 1 and
A21: up1 . 3 = 1 and
A22: P1 = Dir up1 by BKMODEL1:89;
up . 3 = 1 by A19, EUCLID_5:def 3;
then A23: up = up1 by A17, A21, A22, BKMODEL1:43;
reconsider PP = P as Element of BK_model by A4;
consider w being non zero Element of (TOP-REAL 3) such that
A24: Dir w = PP and
A25: w . 3 = 1 and
BK_to_REAL2 PP = |[(w . 1),(w . 2)]| by Def01;
reconsider up2 = |[(- (up `1)),(- (up `2)),1]| as non zero Element of (TOP-REAL 3) by BKMODEL1:41;
( P1 is Element of absolute & P2 is Element of absolute & PP is Element of BK_model & not up1 is zero & not up2 is zero & not w is zero & P1 = Dir up1 & P2 = Dir up2 & PP = Dir w & up1 . 3 = 1 & up2 . 3 = 1 & w . 3 = 1 & up2 . 1 = - (up1 . 1) & up2 . 2 = - (up1 . 2) & P1,PP,P2 are_collinear ) by A22, A18, A24, A21, A25, A23, A2, A3, A5, COLLSP:4, EUCLID_5:def 1, EUCLID_5:def 2;
then consider a being Real such that
A29: ( - 1 < a & a < 1 ) and
A30: ( w . 1 = a * (up1 . 1) & w . 2 = a * (up1 . 2) ) by Th18;
consider d, e, f being Real such that
A31: e = ((d * a) * (up1 . 1)) + ((1 - d) * (- (up1 . 2))) and
A32: f = ((d * a) * (up1 . 2)) + ((1 - d) * (up1 . 1)) and
A33: (e ^2) + (f ^2) = d ^2 by A29, A20, BKMODEL1:16;
d <> 0 by A20, A31, A32, A33;
then not |[e,f,d]| is zero by FINSEQ_1:78, EUCLID_5:4;
then reconsider ur = |[e,f,d]| as non zero Element of (TOP-REAL 3) ;
reconsider S = Dir ur as Element of real_projective_plane by ANPROJ_1:26;
take S ; :: thesis:
A35: qfconic (1,1,(- 1),0,0,0,ur) = 0

proof

qfconic (1,1,(- 1),0,0,0,ur) = ((((((1 * (ur . 1)) * (ur . 1)) + ((1 * (ur . 2)) * (ur . 2))) + (((- 1) * (ur . 3)) * (ur . 3))) + ((0 * (ur . 1)) * (ur . 2))) + ((0 * (ur . 1)) * (ur . 3))) + ((0 * (ur . 2)) * (ur . 3)) by PASCAL:def 1
.= ((e ^2) + (f ^2)) - (d ^2) ;
hence qfconic (1,1,(- 1),0,0,0,ur) = 0 by A33; :: thesis:

end;

|{w,u,ur}| = 0

proof

consider u9 being non zero Element of (TOP-REAL 3) such that
A39: ( P1 = Dir u9 & u9 . 3 = 1 & ((u9 . 1) ^2) + ((u9 . 2) ^2) = 1 & pole_infty P1 = Dir |[(- (u9 . 2)),(u9 . 1),0]| ) by Def03;
up . 3 = 1 by A19, EUCLID_5:def 3;
then A40: u9 = up by A39, A17, BKMODEL1:43;
A41: Q = Dir |[(- (up . 2)),(up . 1),0]| by A39, A40, A16, A6, A9, A10, Th28;
not |[(- (up . 2)),(up . 1),0]| is zero

proof

assume |[(- (up . 2)),(up . 1),0]| is zero ; :: thesis:
then ( up1 . 1 = 0 & up1 . 2 = 0 ) by A23, FINSEQ_1:78, EUCLID_5:4;
hence contradiction by A20; :: thesis:

end;

then are_Prop u,|[(- (up . 2)),(up . 1),0]| by A41, A10, A9, ANPROJ_1:22;
then consider g being Real such that
g <> 0 and
A42: u = g * |[(- (up . 2)),(up . 1),0]| by ANPROJ_1:1;
|[(u `1),(u `2),(u `3)]| = u by EUCLID_5:3
.= |[(g * (- (up . 2))),(g * (up . 1)),(g * 0)]| by A42, EUCLID_5:8 ;
then A43: ( u `1 = g * (- (up . 2)) & u `2 = g * (up . 1) & u `3 = g * 0 ) by FINSEQ_1:78;
A44: w `3 = 1 by A25, EUCLID_5:def 3;
A45: ( w `1 = a * (up1 . 1) & w `2 = a * (up1 . 2) ) by A30, EUCLID_5:def 1, EUCLID_5:def 2;
( ur `1 = e & ur `2 = f & ur `3 = d ) by EUCLID_5:2;
then |{w,u,ur}| = (((((((a * (up1 . 1)) * (g * (up . 1))) * d) - ((1 * (g * (up . 1))) * (((d * a) * (up1 . 1)) + ((1 - d) * (- (up1 . 2)))))) - (((a * (up1 . 1)) * 0) * (((d * a) * (up1 . 2)) + ((1 - d) * (up1 . 1))))) + (((a * (up1 . 2)) * 0) * (((d * a) * (up1 . 1)) + ((1 - d) * (- (up1 . 2)))))) - (((a * (up1 . 2)) * (g * (- (up . 2)))) * d)) + ((1 * (g * (- (up . 2)))) * (((d * a) * (up1 . 2)) + ((1 - d) * (up1 . 1)))) by A43, A44, A45, A31, A32, ANPROJ_8:27
.= 0 by A23 ;
hence |{w,u,ur}| = 0 ; :: thesis:

end;

hence ( S in absolute & P,Q,S are_collinear ) by A35, PASCAL:11, A9, A24, A10, BKMODEL1:1; :: thesis:

end;