let p, q be Element of absolute ; :: thesis:
let a, b be Element of BK_model ; :: thesis:
consider p9 being Element of absolute such that
A1: p <> p9 and
A2: p,a,p9 are_collinear by Th16;
consider q9 being Element of absolute such that
A3: q <> q9 and
A4: q,b,q9 are_collinear by Th16;
consider t being Element of real_projective_plane such that
A5: (tangent p) /\ (tangent p9) = {t} by A1, Th25;
A6: t in (tangent p) /\ (tangent p9) by A5, TARSKI:def 1;
consider u being Element of real_projective_plane such that
A7: (tangent q) /\ (tangent q9) = {u} by A3, Th25;
A8: u in (tangent q) /\ (tangent q9) by A7, TARSKI:def 1;
reconsider a9 = a as Element of real_projective_plane ;
( p <> p9 & a in BK_model & a,p,p9 are_collinear & t in tangent p & t in tangent p9 ) by A1, A2, A6, XBOOLE_0:def 4, COLLSP:4;
then consider Ra being Element of real_projective_plane such that
A9: Ra in absolute and
A10: a9,t,Ra are_collinear by Th31;
reconsider RRa = Ra as Element of absolute by A9;
reconsider b9 = b as Element of real_projective_plane ;
( q <> q9 & b in BK_model & b,q,q9 are_collinear & u in tangent q & u in tangent q9 ) by A3, A4, A8, XBOOLE_0:def 4, COLLSP:4;
then consider Rb being Element of real_projective_plane such that
A11: Rb in absolute and
A12: b9,u,Rb are_collinear by Th31;
reconsider RRb = Rb as Element of absolute by A11;
A13: p,p9,Ra are_mutually_distinct

proof

now :: thesis:

consider ra being Element of real_projective_plane such that
A14: ( ra = Ra & tangent RRa = Line (ra,(pole_infty RRa)) ) by Def04;
thus p <> Ra :: thesis:

proof

assume p = Ra ; :: thesis:
then t in Line (ra,(pole_infty RRa)) by A14, A6, XBOOLE_0:def 4;
then ra, pole_infty RRa,t are_collinear by COLLSP:11;
then A15: ra,t, pole_infty RRa are_collinear by COLLSP:4;
A16: ra,t,a9 are_collinear by A14, A10, HESSENBE:1;
ra <> t

proof

assume ra = t ; :: thesis:
then ( t in absolute & t in tangent p & t in tangent p9 ) by A14, A6, XBOOLE_0:def 4;
then ( t in (tangent p) /\ absolute & t in (tangent p9) /\ absolute ) by XBOOLE_0:def 4;
then ( t in {p} & t in {p9} ) by Th22;
then ( t = p & t = p9 ) by TARSKI:def 1;
hence contradiction by A1; :: thesis:

end;

then ( a in tangent RRa & a in BK_model ) by A16, A15, A14, COLLSP:6, COLLSP:11;
then tangent RRa meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30; :: thesis:

end;

thus p9 <> Ra :: thesis:

proof

assume p9 = Ra ; :: thesis:
then t in Line (ra,(pole_infty RRa)) by A14, A6, XBOOLE_0:def 4;
then ra, pole_infty RRa,t are_collinear by COLLSP:11;
then A17: ra,t, pole_infty RRa are_collinear by COLLSP:4;
A18: ra,t,a9 are_collinear by A14, A10, HESSENBE:1;
ra <> t

proof

end;

then ( a in tangent RRa & a in BK_model ) by A18, A17, A14, COLLSP:6, COLLSP:11;
then tangent RRa meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30; :: thesis:

end;

hence p,p9,Ra are_mutually_distinct by A1; :: thesis:

end;

now :: thesis:

consider rb being Element of real_projective_plane such that
A19: ( rb = Rb & tangent RRb = Line (rb,(pole_infty RRb)) ) by Def04;
thus q <> Rb :: thesis:

proof

assume q = Rb ; :: thesis:
then u in Line (rb,(pole_infty RRb)) by A19, A8, XBOOLE_0:def 4;
then rb, pole_infty RRb,u are_collinear by COLLSP:11;
then A20: rb,u, pole_infty RRb are_collinear by COLLSP:4;
A21: rb,u,b9 are_collinear by A19, A12, HESSENBE:1;
rb <> u

proof

assume rb = u ; :: thesis:
then ( u in absolute & u in tangent q & u in tangent q9 ) by A19, A8, XBOOLE_0:def 4;
then ( u in (tangent q) /\ absolute & u in (tangent q9) /\ absolute ) by XBOOLE_0:def 4;
then ( u in {q} & u in {q9} ) by Th22;
then ( u = q & u = q9 ) by TARSKI:def 1;
hence contradiction by A3; :: thesis:

end;

then ( b in tangent RRb & b in BK_model ) by A21, A20, A19, COLLSP:6, COLLSP:11;
then tangent RRb meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30; :: thesis:

end;

thus q9 <> Rb :: thesis:

proof

assume q9 = Rb ; :: thesis:
then u in Line (rb,(pole_infty RRb)) by A19, A8, XBOOLE_0:def 4;
then rb, pole_infty RRb,u are_collinear by COLLSP:11;
then A22: rb,u, pole_infty RRb are_collinear by COLLSP:4;
A23: rb,u,b9 are_collinear by A19, A12, HESSENBE:1;
rb <> u

proof

end;

then ( b in tangent RRb & b in BK_model ) by A23, A22, A19, COLLSP:6, COLLSP:11;
then tangent RRb meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30; :: thesis:

end;

hence q,q9,Rb are_mutually_distinct by A3; :: thesis:

end;

then consider N being invertible Matrix of 3,F_Real such that
A24: (homography N) .: absolute = absolute and
A25: (homography N) . p = q and
A26: (homography N) . p9 = q9 and
A27: (homography N) . Ra = Rb and
A28: (homography N) . t = u by A9, A11, A6, A8, A13, Th38;
reconsider plp = p, plq = p9, plr = Ra, pls = t, plt = a, np = q, nq = q9, nr = Rb, ns = u, nu = b as Element of real_projective_plane ;

now :: thesis:

thus plp <> plq by A1; :: thesis:
thus np <> nq by A3; :: thesis:
thus nr <> ns :: thesis:

proof

consider rb being Element of real_projective_plane such that
A29: ( rb = Rb & tangent RRb = Line (rb,(pole_infty RRb)) ) by Def04;
rb <> u

proof

assume rb = u ; :: thesis:
then ( u in absolute & u in tangent q & u in tangent q9 ) by A29, A8, XBOOLE_0:def 4;
then ( u in (tangent q) /\ absolute & u in (tangent q9) /\ absolute ) by XBOOLE_0:def 4;
then ( u in {q} & u in {q9} ) by Th22;
then ( u = q & u = q9 ) by TARSKI:def 1;
hence contradiction by A3; :: thesis:

end;

hence nr <> ns by A29; :: thesis:

end;

thus plr <> pls :: thesis:

proof

consider ra being Element of real_projective_plane such that
A30: ( ra = Ra & tangent RRa = Line (ra,(pole_infty RRa)) ) by Def04;
ra <> t

proof

assume ra = t ; :: thesis:
then ( t in absolute & t in tangent p & t in tangent p9 ) by A30, A6, XBOOLE_0:def 4;
then ( t in (tangent p) /\ absolute & t in (tangent p9) /\ absolute ) by XBOOLE_0:def 4;
then ( t in {p} & t in {p9} ) by Th22;
then ( t = p & t = p9 ) by TARSKI:def 1;
hence contradiction by A1; :: thesis:

end;

hence plr <> pls by A30; :: thesis:

end;

thus plp,plq,plt are_collinear by A2, COLLSP:4; :: thesis:
thus plr,pls,plt are_collinear by A10, HESSENBE:1; :: thesis:
thus ( np = (homography N) . plp & nq = (homography N) . plq & nr = (homography N) . plr & ns = (homography N) . pls ) by A25, A26, A27, A28; :: thesis:
thus np,nq,nu are_collinear by A4, HESSENBE:1; :: thesis:
thus nr,ns,nu are_collinear by A12, HESSENBE:1; :: thesis:
thus not plp,plq,plr are_collinear :: thesis:

proof

assume plp,plq,plr are_collinear ; :: thesis:
then p,p9,RRa are_collinear ;
hence contradiction by A13, BKMODEL1:92; :: thesis:

end;

then nu = (homography N) . plt by Th43;
hence ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . a = b & (homography N) . p = q ) by A24, A25; :: thesis: