let AS be AffinSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: LIN x,y,w

now :: thesis: ( x <> y implies LIN x,y,w )

assume A5: x <> y ; :: thesis: 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; :: thesis: verum

end;

hence LIN x,y,w by Th6; :: thesis: verum