:: deftheorem defines up-2-dimensional INCPROJ:def 6 :
for S being IncProjStr holds
( S is up-2-dimensional iff not for p being POINT of S
for P being LINE of S holds p on P );