for P, Q, R being Element of absolute
for P1, P2, P3, P4 being Point of real_projective_plane st P,Q,R are_mutually_distinct & P1 = P & P2 = Q & P3 = R & P4 in tangent P & P4 in tangent Q holds
( not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear )