:: deftheorem defines planar INCSP_1:def 7 :
for S being IncStruct
for F being Subset of the Points of S holds
( F is planar iff ex P being PLANE of S st F on P );