let AS be AffinSpace; :: thesis: for x, y, z, t, u being Element of AS st x <> y & LIN x,y,z & LIN x,y,t & LIN x,y,u holds
LIN z,t,u
let x, y, z, t, u be Element of AS; :: thesis: ( x <> y & LIN x,y,z & LIN x,y,t & LIN x,y,u implies LIN z,t,u )
assume that
A1: x <> y and
A2: LIN x,y,z and
A3: LIN x,y,t and
A4: LIN x,y,u ; :: thesis: LIN z,t,u

A5: now :: thesis: ( x <> z implies LIN z,t,u )

A6: x,y // x,z by A2;
x,y // x,u by A4;
then x,z // x,u by A1, A6, Th4;
then A7: z,x // z,u by DIRAF:40;
x,y // x,t by A3;
then x,z // x,t by A1, A6, Th4;
then A8: z,x // z,t by DIRAF:40;
assume x <> z ; :: thesis: LIN z,t,u
then z,t // z,u by A8, A7, Th4;
hence LIN z,t,u ; :: thesis: verum

end;

( x = z implies LIN z,t,u ) by A1, A3, A4, Th4;
hence LIN z,t,u by A5; :: thesis: verum