for S being IncSpace
for K, L being LINE of S st ( for P being PLANE of S holds
( not K on P or not L on P ) ) holds
K <> L