theorem Th40: :: BKMODEL2:52
for CLSP being CollSp
for p, q being Element of CLSP holds Line (p,q) = Line (q,p)