let AS be AffinSpace; for x, y, z, t being Element of AS st x,y // z,t holds
x,y // t,z
let x, y, z, t be Element of AS; ( x,y // z,t implies x,y // t,z )
assume
x,y // z,t
; x,y // t,z
then
z,t // x,y
by Lm1;
then
t,z // x,y
by Lm2;
hence
x,y // t,z
by Lm1; verum