:: deftheorem Def4 defines transitive COLLSP:def 4 :
for IT being non empty CollStr holds
( IT is transitive iff for a, b, p, q, r being Point of IT st a <> b & [a,b,p] in the Collinearity of IT & [a,b,q] in the Collinearity of IT & [a,b,r] in the Collinearity of IT holds
[p,q,r] in the Collinearity of IT );