:: deftheorem defines at_most-3-dimensional INCPROJ:def 10 :
for IT being IncProjStr holds
( IT is at_most-3-dimensional iff for a being POINT of IT
for M, N being LINE of IT ex b, c being POINT of IT ex S being LINE of IT st
( a on S & b on S & c on S & b on M & c on N ) );