theorem Th1: :: AFF_1:2

for AS being AffinSpace
for x, y being Element of AS holds
( x,y // y,x & x,y // x,y ) by DIRAF:40;