let V be RealLinearSpace; :: thesis: for x1, x2, x3, x4 being Point of V st x1 <> x2 & x1,x2,x3 are_collinear & x1,x2,x4 are_collinear holds
x1,x2,x3,x4 are_collinear
let x1, x2, x3, x4 be Point of V; :: thesis: ( x1 <> x2 & x1,x2,x3 are_collinear & x1,x2,x4 are_collinear implies x1,x2,x3,x4 are_collinear )
assume A1: x1 <> x2 ; :: thesis: ( not x1,x2,x3 are_collinear or not x1,x2,x4 are_collinear or x1,x2,x3,x4 are_collinear )
given L1 being line of V such that A2: ( x1 in L1 & x2 in L1 & x3 in L1 ) ; :: according to RLTOPSP1:def 16 :: thesis: ( not x1,x2,x4 are_collinear or x1,x2,x3,x4 are_collinear )
given L2 being line of V such that A3: ( x1 in L2 & x2 in L2 & x4 in L2 ) ; :: according to RLTOPSP1:def 16 :: thesis: x1,x2,x3,x4 are_collinear
( L1 = Line (x1,x2) & L2 = Line (x1,x2) ) by A1, A2, A3, Th80;
hence ex L being line of V st
( x1 in L & x2 in L & x3 in L & x4 in L ) by A2, A3; :: according to RLTOPSP1:def 17 :: thesis: verum