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