let SAS be Semi_Affine_Space; :: thesis: for a, b, c being Element of SAS st ( a = b or b = c or c = a ) holds
a,b,c is_collinear
let a, b, c be Element of SAS; :: thesis: ( ( a = b or b = c or c = a ) implies a,b,c is_collinear )
assume ( a = b or b = c or c = a ) ; :: thesis: a,b,c is_collinear
then a,b // a,c by Def1, Th12, Th14;
hence a,b,c is_collinear by Def2; :: thesis: verum