:: deftheorem Def8 defines transitive ANPROJ_2:def 8 :
for CS being non empty CollStr holds
( CS is transitive iff for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds
r,r1,r2 are_collinear );