:: deftheorem defines on INCSP_1:def 3 :
for S being IncStruct
for L being LINE of S
for P being PLANE of S holds
( L on P iff [L,P] in the Inc3 of S );