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