theorem Th1: :: INCSP_1:1

for S being IncProjStr
for L being LINE of S
for A, B being POINT of S holds
( {A,B} on L iff ( A on L & B on L ) )