let CLSP be CollSp; :: thesis: for a, b, c being Point of CLSP st ( a = b or a = c or b = c ) holds
a,b,c is_collinear
let a, b, c be Point of CLSP; :: thesis: ( ( a = b or a = c or b = c ) implies a,b,c is_collinear )
assume ( a = b or a = c or b = c ) ; :: thesis: a,b,c is_collinear
then [a,b,c] in the Collinearity of CLSP by Def3;
hence a,b,c is_collinear by Def2; :: thesis: verum