let AS be AffinSpace; for x, y, z, u, w being Element of AS st u <> z & LIN x,y,u & LIN x,y,z & LIN u,z,w holds
LIN x,y,w
let x, y, z, u, w be Element of AS; ( u <> z & LIN x,y,u & LIN x,y,z & LIN u,z,w implies LIN x,y,w )
assume that
A1:
u <> z
and
A2:
LIN x,y,u
and
A3:
LIN x,y,z
and
A4:
LIN u,z,w
; LIN x,y,w
now ( x <> y implies LIN x,y,w )assume A5:
x <> y
;
LIN x,y,w
LIN x,
y,
x
by Th6;
then A6:
LIN z,
u,
x
by A2, A3, A5, Th7;
LIN x,
y,
y
by Th6;
then A7:
LIN z,
u,
y
by A2, A3, A5, Th7;
LIN z,
u,
w
by A4, Th5;
hence
LIN x,
y,
w
by A1, A7, A6, Th7;
verum end;
hence
LIN x,y,w
by Th6; verum