theorem :: PROJPL_1:6

for G being IncProjStr
for a, b, c being POINT of G holds
( a,b,c is_a_triangle iff for P being LINE of G holds
( a |' P or b |' P or c |' P ) ) by Th5;