:: deftheorem Def15 defines with_planes_intersecting_in_2_pts INCSP_1:def 15 :
for S being IncStruct holds
( S is with_planes_intersecting_in_2_pts iff for A being POINT of S
for P, Q being PLANE of S st A on P & A on Q holds
ex B being POINT of S st
( A <> B & B on P & B on Q ) );