:: deftheorem defines at_most-3-dimensional ANPROJ_2:def 15 :
for IT being CollProjectiveSpace holds
( IT is at_most-3-dimensional iff for p, p1, q, q1, r2 being Element of IT ex r, r1 being Element of IT st
( p,q,r are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_collinear ) );