let AS be AffinSpace; :: thesis: for x, y being Element of AS holds
( x,y // y,x & x,y // x,y )
let x, y be Element of AS; :: thesis: ( x,y // y,x & x,y // x,y )
thus x,y // y,x by DIRAF:47; :: thesis: x,y // x,y
y,x // y,y by DIRAF:47;
hence x,y // x,y by DIRAF:47; :: thesis: verum