for AS being AffinSpace
for x, y being Element of AS holds
( LIN x,x,y & LIN x,y,y & LIN x,y,x ) by Th1, Th2;