theorem Th17: :: PROJPL_1:17

for G being IncProjStr st ex a, b, c being POINT of G st a,b,c is_a_triangle & ( for p, q being POINT of G ex M being LINE of G st {p,q} on M ) holds
ex p being POINT of G ex P being LINE of G st p |' P