for S being OAffinSpace
for x, y being Element of S holds
( x,y '||' y,x & x,y '||' x,y ) by Th1;