theorem Th8: :: PROJPL_1:8

for G being IncProjStr
for a being POINT of G
for A being LINE of G st G is IncProjSp holds
ex b, c being POINT of G st
( {b,c} on A & a,b,c are_mutually_distinct )