:: deftheorem Def13 defines with_<=1_plane_per_3_pts INCSP_1:def 13 :
for S being IncStruct holds
( S is with_<=1_plane_per_3_pts iff for A, B, C being POINT of S
for P, Q being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & {A,B,C} on Q holds
P = Q );