let L be LINE of (IncProjSp_of real_projective_plane); :: thesis:
let p, q be POINT of (IncProjSp_of real_projective_plane); :: thesis:
let P, Q be Element of real_projective_plane; :: thesis:
assume that
A1: p = P and
A2: q = Q and
A3: P in BK_model and
A4: Q in absolute and
A5: q on L and
A6: p on L ; :: thesis:
A7: P <> Q by Th01, A3, A4, XBOOLE_0:def 4;
reconsider l = L as LINE of real_projective_plane by INCPROJ:4;
A8: P in l by A1, A6, INCPROJ:5;
reconsider PBK = P as Element of BK_model by A3;
consider R being Element of real_projective_plane such that
A9: R in BK_model and
A10: P <> R and
A11: R,P,Q are_collinear by A3, A4, Th14;
reconsider r = R as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
consider LL being LINE of (IncProjSp_of real_projective_plane) such that
A12: ( r on LL & p on LL & q on LL ) by A1, A2, A11, INCPROJ:10;
L = LL by A1, A2, A5, A6, A12, A7, INCPROJ:8;
then R in l by A12, INCPROJ:5;
then A13: l = Line (P,R) by A8, A10, COLLSP:19;
reconsider RBK = R as Element of BK_model by A9;
consider P1, P2 being Element of absolute such that
A14: P1 <> P2 and
A15: PBK,RBK,P1 are_collinear and
A16: PBK,RBK,P2 are_collinear by A10, Th12;
reconsider PP1 = P1, PP2 = P2 as Element of real_projective_plane ;
A17: ( PP1 in Line (P,R) & PP2 in Line (P,R) ) by A15, A16, COLLSP:11;
reconsider p1 = P1, p2 = P2 as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
( p1 on L & p2 on L ) by A13, A17, INCPROJ:5;
hence ex p1, p2 being POINT of (IncProjSp_of real_projective_plane) ex P1, P2 being Element of real_projective_plane st
( p1 = P1 & p2 = P2 & P1 <> P2 & P1 in absolute & P2 in absolute & p1 on L & p2 on L ) by A14; :: thesis: