theorem Th31: :: DIRAF:31

for S being OAffinSpace
for x, y being Element of S holds
( x,x,y are_collinear & x,y,y are_collinear & x,y,x are_collinear ) by Th19, Th20;