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
Plane (K,L) = Plane (L,K)