:: deftheorem defines 3-dimensional INCPROJ:def 11 :
for IT being IncProjSp holds
( IT is 3-dimensional iff ( IT is at_most-3-dimensional & IT is up-3-dimensional ) );