for IPP being 2-dimensional Desarguesian IncProjSp
for A being LINE of IPP
for x being set holds
( x in CHAIN A iff ex a being POINT of IPP st
( x = a & a on A ) ) ;