let S be OAffinSpace; :: thesis: for u, z, x, y, w being Element of S st u <> z & x,y,u is_collinear & x,y,z is_collinear & u,z,w is_collinear holds
x,y,w is_collinear
let u, z, x, y, w be Element of S; :: thesis: ( u <> z & x,y,u is_collinear & x,y,z is_collinear & u,z,w is_collinear implies x,y,w is_collinear )
assume A1:
( u <> z & x,y,u is_collinear & x,y,z is_collinear & u,z,w is_collinear )
; :: thesis: x,y,w is_collinear
now assume A2:
x <> y
;
:: thesis: x,y,w is_collinear
(
x,
y,
y is_collinear &
x,
y,
x is_collinear )
by Th37;
then
(
z,
u,
y is_collinear &
z,
u,
x is_collinear &
z,
u,
w is_collinear )
by A1, A2, Th36, Th38;
hence
x,
y,
w is_collinear
by A1, Th38;
:: thesis: verum end;
hence
x,y,w is_collinear
by Th37; :: thesis: verum