let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c being Element of FCPS st a,b,c is_collinear holds
( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear )
let a, b, c be Element of FCPS; :: thesis: ( a,b,c is_collinear implies ( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear ) )
assume A1: a,b,c is_collinear ; :: thesis: ( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear )
then A2: b,a,c is_collinear by COLLSP:9;
A3: a,c,b is_collinear by A1, COLLSP:9;
b,c,a is_collinear by A2, COLLSP:9;
hence ( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear ) by A3, COLLSP:9; :: thesis: verum