let V be RealLinearSpace; 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; ( x1 <> x2 & x1,x2,x3 are_collinear & x1,x2,x4 are_collinear implies x1,x2,x3,x4 are_collinear )
assume A1:
x1 <> x2
; ( 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 )
; RLTOPSP1:def 16 ( 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 )
; RLTOPSP1:def 16 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; RLTOPSP1:def 17 verum