:: deftheorem Def9 defines Vebleian ANPROJ_2:def 9 :
for IT being non empty CollStr holds
( IT is Vebleian iff for p, p1, p2, r, r1 being Element of IT st p,p1,r are_collinear & p1,p2,r1 are_collinear holds
ex r2 being Element of IT st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) );