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

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

end;

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