for CLSP being CollSp
for p, q, r, s being Element of CLSP st Line (p,q) = Line (r,s) holds
r,s,p are_collinear by COLLSP:10, COLLSP:11;