:: deftheorem Def3 defines reflexive COLLSP:def 3 :
for IT being non empty CollStr holds
( IT is reflexive iff for a, b, c being Point of IT st ( a = b or a = c or b = c ) holds
[a,b,c] in the Collinearity of IT );