consider a, b, c being Point of CLSP such that
A1: not a,b,c is_collinear by Def6;
take Line a,b ; :: thesis: ex a, b being Point of CLSP st
( a <> b & Line a,b = Line a,b )
a <> b by A1, Th7;
hence ex a, b being Point of CLSP st
( a <> b & Line a,b = Line a,b ) ; :: thesis: verum