let CLSP be proper CollSp; :: thesis: for a, b being Point of CLSP st a <> b holds
Line (a,b) <> the carrier of CLSP
let a, b be Point of CLSP; :: 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 CLSP holds a,b,r are_collinear by Th12;
hence Line (a,b) <> the carrier of CLSP by Th11; :: thesis: verum