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 :: thesis: ( z <> x implies LIN x,y,t )

x,y // x,z by A2;
then x,z // z,t by A1, A3, Th4;
then z,x // z,t by Th3;
then LIN z,x,t ;
then A4: LIN x,z,t by Th5;
assume A5: z <> x ; :: thesis: LIN x,y,t
A6: LIN x,z,x by Th6;
LIN x,z,y by A2, Th5;
hence LIN x,y,t by A5, A4, A6, Th7; :: thesis: verum

end;

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