let FdSp be FanodesSp; :: thesis: for a, b, c being Element of FdSp st a,b,c is_collinear holds
( a,c,b is_collinear & c,b,a is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear )
let a, b, c be Element of FdSp; :: thesis: ( a,b,c is_collinear implies ( a,c,b is_collinear & c,b,a is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear ) )
assume a,b,c is_collinear ; :: thesis: ( a,c,b is_collinear & c,b,a is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear )
then A1: a,b '||' a,c by Def2;
then A2: ( b,a '||' b,c & b,c '||' b,a ) by PARSP_1:24;
A3: c,a '||' c,b by A1, PARSP_1:24;
( a,c '||' a,b & c,b '||' c,a ) by A1, PARSP_1:24;
hence ( a,c,b is_collinear & c,b,a is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear ) by A2, A3, Def2; :: thesis: verum