:: deftheorem Def9 defines linear INCSP_1:def 9 :
for S being IncProjStr holds
( S is linear iff for A, B being POINT of S ex L being LINE of S st {A,B} on L );