let PCPP be CollProjectiveSpace; :: thesis: for a, b, c being Element of PCPP st a,b,c are_collinear holds
( b,c,a are_collinear & c,a,b are_collinear & b,a,c are_collinear & a,c,b are_collinear & c,b,a are_collinear )
let a, b, c be Element of PCPP; :: thesis: ( a,b,c are_collinear implies ( b,c,a are_collinear & c,a,b are_collinear & b,a,c are_collinear & a,c,b are_collinear & c,b,a are_collinear ) )
assume A1: a,b,c are_collinear ; :: thesis: ( b,c,a are_collinear & c,a,b are_collinear & b,a,c are_collinear & a,c,b are_collinear & c,b,a are_collinear )
then b,a,c are_collinear by COLLSP:4;
then A2: b,c,a are_collinear by COLLSP:4;
a,c,b are_collinear by A1, COLLSP:4;
hence ( b,c,a are_collinear & c,a,b are_collinear & b,a,c are_collinear & a,c,b are_collinear & c,b,a are_collinear ) by A2, COLLSP:4; :: thesis: verum