:: deftheorem Def20 defines Plane INCSP_1:def 20 :
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
for b₅ being PLANE of S holds
( b₅ = Plane (A,B,C) iff {A,B,C} on b₅ );