consider a, b, c being Point of CLSP such that
A1: not a,b,c are_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, Th2;
hence ex a, b being Point of CLSP st
( a <> b & Line (a,b) = Line (a,b) ) ; :: thesis: verum