:: deftheorem defines CHAIN PROJRED2:def 2 :
for IPS being IncProjSp
for Z being LINE of IPS holds CHAIN Z = { z where z is POINT of IPS : z on Z } ;