for G being IncProjStr
for a1, a2, b being POINT of G
for A being LINE of G st G is configuration & {a1,a2} on A & a1 <> a2 & b |' A holds
a1,a2,b is_a_triangle