:: deftheorem Def14 defines with_lines_inside_planes INCSP_1:def 14 :
for S being IncStruct holds
( S is with_lines_inside_planes iff for L being LINE of S
for P being PLANE of S st ex A, B being POINT of S st
( A <> B & {A,B} on L & {A,B} on P ) holds
L on P );