let P be Element of BK_model ; for Q being Element of absolute ex R being Element of absolute st
( Q <> R & Q,P,R are_collinear )
let Q be Element of absolute ; ex R being Element of absolute st
( Q <> R & Q,P,R are_collinear )
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;