let CLSP be proper CollSp; :: thesis: for a, b being Point of st a <> b holds
Line a,b <> the carrier of CLSP
let a, b be Point of ; :: thesis: ( a <> b implies Line a,b <> the carrier of CLSP )
assume a <> b ; :: thesis: Line a,b <> the carrier of CLSP
then not for r being Point of holds a,b,r is_collinear by Th19;
hence Line a,b <> the carrier of CLSP by Th17; :: thesis: verum