let P be Element of BK_model ; :: thesis: for L being LINE of (IncProjSp_of real_projective_plane) 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 (IncProjSp_of real_projective_plane); :: 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 (ProjectiveSpace (TOP-REAL 3)) 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 A2, BKMODEL2:19;

reconsider p = P, r = R as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;

reconsider L9 = L as LINE of real_projective_plane by INCPROJ:4;

Line (P,Q) = L9 by A1, A2, A3, COLLSP:19;

then ( P in L9 & Q in L9 & R in L9 ) by A1, A3, A4, COLLSP:11;

then ( p on L & r 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

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 A5, A6, A10, A11, INCPROJ:5;

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

ex P1, P2 being Element of absolute st

( P1 <> P2 & P1 in L & P2 in L )

let L be LINE of (IncProjSp_of real_projective_plane); :: 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 (ProjectiveSpace (TOP-REAL 3)) 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 A2, BKMODEL2:19;

reconsider p = P, r = R as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;

reconsider L9 = L as LINE of real_projective_plane by INCPROJ:4;

Line (P,Q) = L9 by A1, A2, A3, COLLSP:19;

then ( P in L9 & Q in L9 & R in L9 ) by A1, A3, A4, COLLSP:11;

then ( p on L & r 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

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 A5, A6, A10, A11, INCPROJ:5;

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