let CLSP be CollSp; :: thesis: for a, b, c being Point of CLSP st a,b,c is_collinear holds
b,c,a is_collinear
let a, b, c be Point of CLSP; :: thesis: ( a,b,c is_collinear implies b,c,a is_collinear )
assume a,b,c is_collinear ; :: thesis: b,c,a is_collinear
then b,a,c is_collinear by Th9;
hence b,c,a is_collinear by Th9; :: thesis: verum