for S being IncSpace
for A being POINT of S
for L being LINE of S ex B being POINT of S st
( A <> B & B on L ) by Lm1;