for S being IncSpace
for L being LINE of S
for P being PLANE of S
for F being Subset of the Points of S st F on L & L on P holds
F on P by Def17;