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 ) )
; ( ( 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 )
; CS is reflexive
let p, q, r be Element of CS; COLLSP:def 3 ( ( 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 )
; [p,q,r] in the Collinearity of CS