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

now

x,y // x,z by A2, Def1;
then x,z // z,t by A1, A3, Th14;
then z,x // z,t by Th13;
then LIN z,x,t by Def1;
then A4: LIN x,z,t by Th15;
assume A5: z <> x ; :: thesis: LIN x,y,t
A6: LIN x,z,x by Th16;
LIN x,z,y by A2, Th15;
hence LIN x,y,t by A5, A4, A6, Th17; :: thesis: verum

end;

hence LIN x,y,t by A3, Def1; :: thesis: verum