let P be Element of BK_model ; :: thesis: for L being LINE of st P in L holds
ex P1, P2 being Element of absolute st
( P1 <> P2 & P1 in L & P2 in L )

let L be LINE of ; :: thesis: ( P in L implies ex P1, P2 being Element of absolute st
( P1 <> P2 & P1 in L & P2 in L ) )

assume A1: P in L ; :: thesis: ex P1, P2 being Element of absolute st
( P1 <> P2 & P1 in L & P2 in L )

consider Q being Element of () such that
A2: P <> Q and
A3: Q in L by BKMODEL2:8;
consider R being Element of absolute such that
A4: P,Q,R are_collinear by ;
reconsider p = P, r = R as POINT of by INCPROJ:3;
reconsider L9 = L as LINE of real_projective_plane by INCPROJ:4;
Line (P,Q) = L9 by ;
then ( P in L9 & Q in L9 & R in L9 ) by ;
then ( p on L & r on L ) by INCPROJ:5;
then consider p1, p2 being POINT of , P1, P2 being Element of real_projective_plane such that
A5: p1 = P1 and
A6: p2 = P2 and
A7: P1 <> P2 and
A8: P1 in absolute and
A9: P2 in absolute and
A10: p1 on L and
A11: p2 on L by BKMODEL2:23;
reconsider P1 = P1, P2 = P2 as Element of absolute by A8, A9;
take P1 ; :: thesis: ex P2 being Element of absolute st
( P1 <> P2 & P1 in L & P2 in L )

take P2 ; :: thesis: ( P1 <> P2 & P1 in L & P2 in L )
( P1 in L9 & P2 in L9 ) by ;
hence ( P1 <> P2 & P1 in L & P2 in L ) by A7; :: thesis: verum