:: deftheorem defines on INCSP_1:def 1 :
for S being IncProjStr
for A being POINT of S
for L being LINE of S holds
( A on L iff [A,L] in the Inc of S );