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

now :: thesis: ( x <> y implies x,y // z,t )

A3: x,y // x,t by A2;
A4: x,y // x,z by A1;
assume x <> y ; :: thesis: x,y // z,t
then x,z // x,t by A4, A3, Th4;
then z,x // z,t by DIRAF:40;
then x,z // z,t by Th3;
hence x,y // z,t by A4, A3, Th4; :: thesis: verum

end;

hence x,y // z,t by Th2; :: thesis: verum