let AS be AffinSpace; :: thesis: for x, y, z, t being Element of AS st x,y // z,t holds
y,x // z,t
let x, y, z, t be Element of AS; :: thesis: ( x,y // z,t implies y,x // z,t )
assume A1: x,y // z,t ; :: thesis: y,x // z,t
x,y // y,x by Th1;
then ( y,x // z,t or x = y ) by A1, DIRAF:40;
hence y,x // z,t by Th2; :: thesis: verum