thus
( CS is reflexive implies for p, q, r being Element of CS holds

( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear ) ) ; :: thesis: ( ( for p, q, r being Element of CS holds

( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear ) ) implies CS is reflexive )

assume A1: for p, q, r being Element of CS holds

( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_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 A2: ( p = q or p = r or q = r ) ; :: thesis: [p,q,r] in the Collinearity of CS

( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear ) ) ; :: thesis: ( ( for p, q, r being Element of CS holds

( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear ) ) implies CS is reflexive )

assume A1: for p, q, r being Element of CS holds

( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_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 A2: ( p = q or p = r or q = r ) ; :: thesis: [p,q,r] in the Collinearity of CS