let AS be AffinSpace; :: thesis: 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; :: thesis: ( x,y // z,t implies x,y // t,z )
assume x,y // z,t ; :: thesis: 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; :: thesis: verum