let P, Q, R be Element of absolute ; :: thesis:
let P1, P2, P3, P4 be Point of real_projective_plane; :: thesis:
assume that
A1: P,Q,R are_mutually_distinct and
A2: ( P1 = P & P2 = Q & P3 = R ) and
A3: P4 in tangent P and
A4: P4 in tangent Q ; :: thesis:
A5: not P4 in absolute

assume P4 in absolute ; :: thesis:
then ( P4 in absolute /\ (tangent P) & P4 in absolute /\ (tangent Q) ) by A3, A4, XBOOLE_0:def 4;
then ( P4 in {P} & P4 in {Q} ) by Th22;
then ( P4 = P & P4 = Q ) by TARSKI:def 1;
hence contradiction by A1; :: thesis:

end;

consider p being Element of real_projective_plane such that
A6: p = P and
A7: tangent P = Line (p,(pole_infty P)) by Def04;
A8: p, pole_infty P,P4 are_collinear by A3, A7, COLLSP:11;
A9: P4 <> p by A6, A5;
consider q being Element of real_projective_plane such that
A10: q = Q and
A11: tangent Q = Line (q,(pole_infty Q)) by Def04;
A12: P4 <> q by A10, A5;
A13: q, pole_infty Q,P4 are_collinear by A4, A11, COLLSP:11;
thus not P1,P2,P3 are_collinear by A1, A2, BKMODEL1:92; :: thesis:
thus not P1,P2,P4 are_collinear :: thesis:

assume A14: P1,P2,P4 are_collinear ; :: thesis:

thus P4 <> p by A6, A5; :: thesis:
thus P4,p,p are_collinear by COLLSP:2; :: thesis:
p,P4, pole_infty P are_collinear by A8, COLLSP:4;
hence P4,p, pole_infty P are_collinear by COLLSP:7; :: thesis:
p,P4,q are_collinear by A14, A2, A6, A10, COLLSP:4;
hence P4,p,q are_collinear by COLLSP:4; :: thesis:

end;

then Q in tangent P by A10, A7, COLLSP:3, COLLSP:11;
then Q in absolute /\ (tangent P) by XBOOLE_0:def 4;
then Q in {P} by Th22;
hence contradiction by A1, TARSKI:def 1; :: thesis:

end;

thus not P1,P3,P4 are_collinear :: thesis:

assume P1,P3,P4 are_collinear ; :: thesis:
then A15: p,P4,P3 are_collinear by A2, A6, COLLSP:4;
p,P4, pole_infty P are_collinear by A8, COLLSP:4;
then P3 in tangent P by A9, A15, A7, COLLSP:6, COLLSP:11;
then P3 in absolute /\ (tangent P) by A2, XBOOLE_0:def 4;
then P3 in {P} by Th22;
hence contradiction by A1, A2, TARSKI:def 1; :: thesis:

end;

thus not P2,P3,P4 are_collinear :: thesis:

assume P2,P3,P4 are_collinear ; :: thesis:
then A16: q,P4,P3 are_collinear by A2, A10, COLLSP:4;
q,P4, pole_infty Q are_collinear by A13, COLLSP:4;
then P3 in tangent Q by A16, A12, A11, COLLSP:6, COLLSP:11;
then P3 in absolute /\ (tangent Q) by A2, XBOOLE_0:def 4;
then P3 in {Q} by Th22;
hence contradiction by A1, A2, TARSKI:def 1; :: thesis:

end;