for CLSP being proper CollSp
for P being LINE of CLSP ex a, b being Point of CLSP st
( a <> b & a in P & b in P )