theorem ThAZ9: :: GTARSKI2:41

for P, Q, R being Point of (TOP-REAL 2)
for L being Element of line_of_REAL 2 st P in L & Q in L & R in L & not P in LSeg (Q,R) & not Q in LSeg (R,P) holds
R in LSeg (P,Q)