:: deftheorem defines up-3-rank INCPROJ:def 7 :
for S being IncProjStr holds
( S is up-3-rank iff for P being LINE of S ex a, b, c being POINT of S st
( a <> b & b <> c & c <> a & a on P & b on P & c on P ) );