let P be Element of BK_model ; :: thesis:
let Q be Element of absolute ; :: thesis:
A1: P <> Q by XBOOLE_0:def 4, Th01;
reconsider p9 = P, q9 = Q as Element of real_projective_plane ;
reconsider L9 = Line (p9,q9) as LINE of real_projective_plane by A1, COLLSP:def 7;
reconsider L = L9 as LINE of (IncProjSp_of real_projective_plane) by INCPROJ:4;
reconsider p = P, q = Q as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
( p9 in L9 & q9 in L9 ) by COLLSP:10;
then ( p on L & q on L ) by INCPROJ:5;
then consider p1, p2 being POINT of (IncProjSp_of real_projective_plane), P1, P2 being Element of real_projective_plane such that
A2: ( p1 = P1 & p2 = P2 & P1 <> P2 & P1 in absolute & P2 in absolute & p1 on L & p2 on L ) by Th15;
reconsider p1 = p1, p2 = p2 as Element of real_projective_plane by INCPROJ:3;
A3: ( P1 in L9 & P2 in L9 ) by A2, INCPROJ:5;
then A4: ( p9,q9,p1 are_collinear & p9,q9,p2 are_collinear & P1 <> P2 & P1 in absolute & P2 in absolute ) by A2, COLLSP:11;
reconsider P1 = P1, P2 = P2 as Element of absolute by A2;

per cases ;

suppose A5: q9 = p1 ; :: thesis:

take P2 ; :: thesis:

now :: thesis:

thus Q <> P2 by A5, A2; :: thesis:
P,Q,P2 are_collinear by A3, COLLSP:11;
hence Q,P,P2 are_collinear by COLLSP:4; :: thesis:

end;

hence ( Q <> P2 & Q,P,P2 are_collinear ) ; :: thesis:

end;

suppose q9 <> p1 ; :: thesis:

per cases ;

suppose A6: Q <> P2 ; :: thesis:

take P2 ; :: thesis:
P,Q,P2 are_collinear by A3, COLLSP:11;
hence ( Q <> P2 & Q,P,P2 are_collinear ) by A6, COLLSP:4; :: thesis:

end;

suppose A7: Q = P2 ; :: thesis:

take P1 ; :: thesis:
thus ( Q <> P1 & Q,P,P1 are_collinear ) by A4, A7, A2, COLLSP:4; :: thesis:

end;

end;

end;

end;