for G being IncProjSp
for a, b, c being POINT of G st a,b,c is_a_triangle holds
a,b,c are_mutually_distinct