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