let CLSP be CollSp; :: thesis: 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; :: thesis: ( a,b,c are_collinear implies b,c,a are_collinear )
assume a,b,c are_collinear ; :: thesis: b,c,a are_collinear
then b,a,c are_collinear by Th4;
hence b,c,a are_collinear by Th4; :: thesis: verum