:: deftheorem defines on INCSP_1:def 2 :
for S being IncStruct
for A being POINT of S
for P being PLANE of S holds
( A on P iff [A,P] in the Inc2 of S );