let FdSp be FanodesSp; :: thesis: for a, b, c being Element of FdSp st ( a = b or b = c or c = a ) holds
a,b,c is_collinear
let a, b, c be Element of FdSp; :: 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 PARSP_1:25;
hence a,b,c is_collinear by Def2; :: thesis: verum