let AS be AffinSpace; :: thesis: for u, z, x, y, 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 u, z, x, y, 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 Th7;
then A6: LIN z,u,x by A2, A3, A5, Th8;
LIN x,y,y by Th7;
then A7: LIN z,u,y by A2, A3, A5, Th8;
LIN z,u,w by A4, Th6;
hence LIN x,y,w by A1, A7, A6, Th8; :: thesis: verum

end;

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