theorem Th27:
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 )