let CLSP be CollSp; for a, b, c being Point of CLSP st a,b,c are_collinear holds
b,c,a are_collinear
let a, b, c be Point of CLSP; ( a,b,c are_collinear implies b,c,a are_collinear )
assume
a,b,c are_collinear
; b,c,a are_collinear
then
b,a,c are_collinear
by Th4;
hence
b,c,a are_collinear
by Th4; verum