hereby :: thesis: ( ( for p, q, r being Element of CS holds
( p,q,p is_collinear & p,p,q is_collinear & p,q,q is_collinear ) ) implies CS is reflexive )

assume A1: CS is reflexive ; :: thesis: for p, q, r being Element of CS holds
( p,q,p is_collinear & p,p,q is_collinear & p,q,q is_collinear )
let p, q, r be Element of CS; :: thesis: ( p,q,p is_collinear & p,p,q is_collinear & p,q,q is_collinear )
[p,q,p] in the Collinearity of CS by A1, COLLSP:def 3;
hence p,q,p is_collinear by COLLSP:def 2; :: thesis: ( p,p,q is_collinear & p,q,q is_collinear )
[p,p,q] in the Collinearity of CS by A1, COLLSP:def 3;
hence p,p,q is_collinear by COLLSP:def 2; :: thesis: p,q,q is_collinear
[p,q,q] in the Collinearity of CS by A1, COLLSP:def 3;
hence p,q,q is_collinear by COLLSP:def 2; :: thesis: verum

end;

assume A2: for p, q, r being Element of CS holds
( p,q,p is_collinear & p,p,q is_collinear & p,q,q is_collinear ) ; :: thesis: CS is reflexive
let p, q, r be Element of CS; :: according to COLLSP:def 3 :: thesis: ( ( not p = q & not p = r & not q = r ) or [p,q,r] in the Collinearity of CS )
assume A3: ( p = q or p = r or q = r ) ; :: thesis: [p,q,r] in the Collinearity of CS

per cases ( p = q or p = r or q = r ) by A3;

suppose p = q ; :: thesis: [p,q,r] in the Collinearity of CS

then p,q,r is_collinear by A2;
hence [p,q,r] in the Collinearity of CS by COLLSP:def 2; :: thesis: verum

end;

suppose p = r ; :: thesis: [p,q,r] in the Collinearity of CS

then p,q,r is_collinear by A2;
hence [p,q,r] in the Collinearity of CS by COLLSP:def 2; :: thesis: verum

end;

suppose q = r ; :: thesis: [p,q,r] in the Collinearity of CS

then p,q,r is_collinear by A2;
hence [p,q,r] in the Collinearity of CS by COLLSP:def 2; :: thesis: verum

end;

end;