for S being IncSpace
for P, Q being PLANE of S holds
( not P <> Q or for A being POINT of S holds
( not A on P or not A on Q ) or ex L being LINE of S st
for B being POINT of S holds
( ( B on P & B on Q ) iff B on L ) )