let CLSP be CollSp; :: thesis: for a, b being Point of CLSP holds
( a in Line (a,b) & b in Line (a,b) )
let a, b be Point of CLSP; :: thesis: ( a in Line (a,b) & b in Line (a,b) )
a,b,a are_collinear by Th2;
hence a in Line (a,b) ; :: thesis: b in Line (a,b)
a,b,b are_collinear by Th2;
hence b in Line (a,b) ; :: thesis: verum