let P, R, S be Element of real_projective_plane; :: thesis: for Q being Element of absolute st P in BK_model & R in tangent Q & P,S,R are_collinear & R <> S holds
Q <> S
let Q be Element of absolute ; :: thesis: ( P in BK_model & R in tangent Q & P,S,R are_collinear & R <> S implies Q <> S )
assume that
A1: P in BK_model and
A2: R in tangent Q and
A3: P,S,R are_collinear and
A4: R <> S ; :: thesis: Q <> S
A5: S,R,P are_collinear by A3, COLLSP:8;
consider q being Element of real_projective_plane such that
A6: ( q = Q & tangent Q = Line (q,(pole_infty Q)) ) by Def04;
assume Q = S ; :: thesis: contradiction
then ( q, pole_infty Q,S are_collinear & q, pole_infty Q,R are_collinear ) by A2, Th21, A6, COLLSP:11;
then A7: P in tangent Q by A5, A4, COLLSP:9, A6, COLLSP:11;
reconsider L = tangent Q as LINE of (IncProjSp_of real_projective_plane) by INCPROJ:4;
reconsider ip = P, iq = Q as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
Q in tangent Q by Th21;
then ( ip on L & iq on L ) by A7, INCPROJ:5;
then consider p1, p2 being POINT of (IncProjSp_of real_projective_plane), P1, P2 being Element of real_projective_plane such that
A8: ( p1 = P1 & p2 = P2 & P1 <> P2 & P1 in absolute & P2 in absolute & p1 on L & p2 on L ) by A1, Th15;
( P1 in L & P2 in L ) by A8, INCPROJ:5;
then ( P1 in (tangent Q) /\ absolute & P2 in (tangent Q) /\ absolute ) by A8, XBOOLE_0:def 4;
then ( P1 in {Q} & P2 in {Q} ) by Th22;
then ( P1 = Q & P2 = Q ) by TARSKI:def 1;
hence contradiction by A8; :: thesis: verum