:: deftheorem Def22 defines Plane INCSP_1:def 22 :
for S being IncSpace
for K, L being LINE of S st K <> L & ex A being POINT of S st
( A on K & A on L ) holds
for b₄ being PLANE of S holds
( b₄ = Plane (K,L) iff ( K on b₄ & L on b₄ ) );