let AS be AffinSpace; for x, y, z, t being Element of AS st x,y // z,t holds
z,t // x,y
let x, y, z, t be Element of AS; ( x,y // z,t implies z,t // x,y )
assume A1:
x,y // z,t
; z,t // x,y
now ( x <> y implies z,t // x,y )end;
hence
z,t // x,y
by DIRAF:40; verum