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

assume A5: x <> y ; :: thesis: LIN x,y,w
LIN x,y,x by Th16;
then A6: LIN z,u,x by A2, A3, A5, Th17;
LIN x,y,y by Th16;
then A7: LIN z,u,y by A2, A3, A5, Th17;
LIN z,u,w by A4, Th15;
hence LIN x,y,w by A1, A7, A6, Th17; :: thesis: verum

end;

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