let P, Q be Element of BK_model ; :: thesis:
assume A1: P <> Q ; :: thesis:
then consider P1, P2 being Element of absolute such that
A2: P1 <> P2 and
A3: P,Q,P1 are_collinear and
A4: P,Q,P2 are_collinear by Th12;
consider R being Element of real_projective_plane such that
A5: ( R in tangent P1 & R in tangent P2 ) by Th24;
consider u being Element of (TOP-REAL 3) such that
A6: not u is zero and
A7: R = Dir u by ANPROJ_1:26;

per cases ;

suppose u . 3 = 0 ; :: thesis:

reconsider RR = R as Element of (ProjectiveSpace (TOP-REAL 3)) ;
P,P1,P2 are_collinear by A1, A3, A4, COLLSP:6;
then consider PT1 being Element of (ProjectiveSpace (TOP-REAL 3)) such that
A8: PT1 in absolute and
A9: P,RR,PT1 are_collinear by A2, A5, Th31;
( Q,P,P1 are_collinear & Q,P,P2 are_collinear ) by A3, A4, COLLSP:4;
then Q,P1,P2 are_collinear by A1, COLLSP:6;
then consider PT2 being Element of (ProjectiveSpace (TOP-REAL 3)) such that
A10: PT2 in absolute and
A11: Q,RR,PT2 are_collinear by A2, A5, Th31;

now :: thesis:

thus P,Q,P1 are_collinear by A3; :: thesis:
thus P,Q,P2 are_collinear by A4; :: thesis:
A12: PT1 <> RR

proof

assume PT1 = RR ; :: thesis:
then ( PT1 in absolute /\ (tangent P1) & PT1 in absolute /\ (tangent P2) ) by A5, A8, XBOOLE_0:def 4;
then ( PT1 in {P1} & PT1 in {P2} ) by Th22;
then ( PT1 = P1 & PT1 = P2 ) by TARSKI:def 1;
hence contradiction by A2; :: thesis:

end;

A13: PT2 <> RR

proof

assume PT2 = RR ; :: thesis:
then ( PT2 in absolute /\ (tangent P1) & PT2 in absolute /\ (tangent P2) ) by A5, A10, XBOOLE_0:def 4;
then ( PT2 in {P1} & PT2 in {P2} ) by Th22;
then ( PT2 = P1 & PT2 = P2 ) by TARSKI:def 1;
hence contradiction by A2; :: thesis:

end;

A14: P2 <> PT1

proof

P,PT1,RR are_collinear by A9, COLLSP:4;
hence P2 <> PT1 by A5, A12, Th32; :: thesis:

end;

P1 <> PT1

proof

assume A15: P1 = PT1 ; :: thesis:
consider p1 being Element of real_projective_plane such that
A16: ( p1 = P1 & tangent P1 = Line (p1,(pole_infty P1)) ) by Def04;
reconsider pt1 = PT1, rr = RR, p = P as Element of real_projective_plane ;
A17: ( p1, pole_infty P1,pt1 are_collinear & p1, pole_infty P1,rr are_collinear ) by A15, A5, Th21, A16, COLLSP:11;
rr,pt1,p are_collinear by A9, COLLSP:8;
then ( P in tangent P1 & P in BK_model ) by A12, A17, A16, COLLSP:9, COLLSP:11;
then tangent P1 meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30; :: thesis:

end;

hence P1,P2,PT1 are_mutually_distinct by A14, A2; :: thesis:
A18: P1 <> PT2

proof

Q,PT2,RR are_collinear by A11, COLLSP:4;
hence P1 <> PT2 by A5, A13, Th32; :: thesis:

end;

P2 <> PT2

proof

assume A19: P2 = PT2 ; :: thesis:
consider p2 being Element of real_projective_plane such that
A20: ( p2 = P2 & tangent P2 = Line (p2,(pole_infty P2)) ) by Def04;
reconsider pt2 = PT2, rr = RR, q = Q as Element of real_projective_plane ;
A21: ( p2, pole_infty P2,pt2 are_collinear & p2, pole_infty P2,rr are_collinear ) by A20, A19, A5, Th21, COLLSP:11;
rr,pt2,q are_collinear by A11, COLLSP:8;
then ( Q in tangent P2 & Q in BK_model ) by A20, A13, A21, COLLSP:9, COLLSP:11;
then tangent P2 meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30; :: thesis:

end;

hence P1,P2,PT2 are_mutually_distinct by A18, A2; :: thesis:
thus R in (tangent P1) /\ (tangent P2) by A5, XBOOLE_0:def 4; :: thesis:
thus P,RR,PT1 are_collinear by A9; :: thesis:
thus Q,RR,PT2 are_collinear by A11; :: thesis:

end;

hence ex P1, P2, P3, P4 being Element of absolute ex P5 being Element of (ProjectiveSpace (TOP-REAL 3)) st
( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & P,P5,P3 are_collinear & Q,P5,P4 are_collinear & P1,P2,P3 are_mutually_distinct & P1,P2,P4 are_mutually_distinct & P5 in (tangent P1) /\ (tangent P2) ) by A8, A10; :: thesis:

end;

suppose A22: 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;
A23: v . 3 = v `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ;
A24: ( (u . 3) * ((u . 1) / (u . 3)) = u . 1 & (u . 3) * ((u . 2) / (u . 3)) = u . 2 ) by A22, 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 `1),(u . 2),(u . 3)]| by A24, EUCLID_5:def 1
.= |[(u `1),(u `2),(u . 3)]| by EUCLID_5:def 2
.= |[(u `1),(u `2),(u `3)]| by EUCLID_5:def 3
.= u by EUCLID_5:3 ;
then are_Prop v,u by A22, ANPROJ_1:1;
then A25: ( R = Dir v & v . 3 = 1 ) by A6, A7, A23, ANPROJ_1:22;
reconsider RR = R as Element of (ProjectiveSpace (TOP-REAL 3)) ;
P <> RR

proof

assume P = RR ; :: thesis:
then BK_model meets tangent P1 by A5, XBOOLE_0:def 4;
hence contradiction by Th30; :: thesis:

end;

then consider PT1 being Element of absolute such that
A26: P,RR,PT1 are_collinear by A25, Th03;
Q <> RR

proof

assume Q = RR ; :: thesis:
then BK_model meets tangent P2 by A5, XBOOLE_0:def 4;
hence contradiction by Th30; :: thesis:

end;

then consider PT2 being Element of absolute such that
A27: Q,RR,PT2 are_collinear by A25, Th03;

now :: thesis:

thus P,Q,P1 are_collinear by A3; :: thesis:
thus P,Q,P2 are_collinear by A4; :: thesis:
A28: PT1 <> RR

proof

assume PT1 = RR ; :: thesis:
then ( PT1 in absolute /\ (tangent P1) & PT1 in absolute /\ (tangent P2) ) by A5, XBOOLE_0:def 4;
then ( PT1 in {P1} & PT1 in {P2} ) by Th22;
then ( PT1 = P1 & PT1 = P2 ) by TARSKI:def 1;
hence contradiction by A2; :: thesis:

end;

A29: PT2 <> RR

proof

assume PT2 = RR ; :: thesis:
then ( PT2 in absolute /\ (tangent P1) & PT2 in absolute /\ (tangent P2) ) by A5, XBOOLE_0:def 4;
then ( PT2 in {P1} & PT2 in {P2} ) by Th22;
then ( PT2 = P1 & PT2 = P2 ) by TARSKI:def 1;
hence contradiction by A2; :: thesis:

end;

A30: P2 <> PT1

proof

P,PT1,RR are_collinear by A26, COLLSP:4;
hence P2 <> PT1 by A5, A28, Th32; :: thesis:

end;

P1 <> PT1

proof

assume A31: P1 = PT1 ; :: thesis:
consider p1 being Element of real_projective_plane such that
A32: ( p1 = P1 & tangent P1 = Line (p1,(pole_infty P1)) ) by Def04;
reconsider pt1 = PT1, rr = RR, p = P as Element of real_projective_plane ;
A33: ( p1, pole_infty P1,pt1 are_collinear & p1, pole_infty P1,rr are_collinear ) by A31, A5, Th21, A32, COLLSP:11;
rr,pt1,p are_collinear by A26, COLLSP:8;
then ( P in tangent P1 & P in BK_model ) by A28, A33, A32, COLLSP:9, COLLSP:11;
then tangent P1 meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30; :: thesis:

end;

hence P1,P2,PT1 are_mutually_distinct by A30, A2; :: thesis:
A34: P1 <> PT2

proof

Q,PT2,RR are_collinear by A27, COLLSP:4;
hence P1 <> PT2 by A5, A29, Th32; :: thesis:

end;

P2 <> PT2

proof

assume A35: P2 = PT2 ; :: thesis:
consider p2 being Element of real_projective_plane such that
A36: ( p2 = P2 & tangent P2 = Line (p2,(pole_infty P2)) ) by Def04;
reconsider pt2 = PT2, rr = RR, q = Q as Element of real_projective_plane ;
A37: ( p2, pole_infty P2,pt2 are_collinear & p2, pole_infty P2,rr are_collinear ) by A35, A5, Th21, A36, COLLSP:11;
rr,pt2,q are_collinear by A27, COLLSP:8;
then Q in tangent P2 by A36, A29, A37, COLLSP:9, COLLSP:11;
then tangent P2 meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30; :: thesis:

end;

hence P1,P2,PT2 are_mutually_distinct by A34, A2; :: thesis:
thus RR in (tangent P1) /\ (tangent P2) by A5, XBOOLE_0:def 4; :: thesis:
thus P,RR,PT1 are_collinear by A26; :: thesis:
thus Q,RR,PT2 are_collinear by A27; :: thesis:

end;