let P, Q, R be Point of (TOP-REAL 2); :: thesis: 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)
let L be Element of line_of_REAL 2; :: thesis: ( P in L & Q in L & R in L & not P in LSeg (Q,R) & not Q in LSeg (R,P) implies R in LSeg (P,Q) )
assume that
A1: P in L and
A2: Q in L and
A3: R in L ; :: thesis: ( P in LSeg (Q,R) or Q in LSeg (R,P) or R in LSeg (P,Q) )
L in line_of_REAL 2 ;
then L in { (Line (x1,x2)) where x1, x2 is Element of REAL 2 : verum } by EUCLIDLP:def 4;
then consider x1, x2 being Element of REAL 2 such that
A4: L = Line (x1,x2) ;
reconsider tx1 = x1, tx2 = x2 as Element of (TOP-REAL 2) by EUCLID:22;
( P in Line (tx1,tx2) & Q in Line (tx1,tx2) & R in Line (tx1,tx2) ) by A1, A2, A3, A4, EUCLID12:4;
hence ( P in LSeg (Q,R) or Q in LSeg (R,P) or R in LSeg (P,Q) ) by RLTOPSP1:def 16, TOPREAL9:67; :: thesis: verum