let G be IncProjSp; :: thesis: for a, b, c being POINT of G st a,b,c is_a_triangle holds
a,b,c are_mutually_different
let a, b, c be POINT of G; :: thesis: ( a,b,c is_a_triangle implies a,b,c are_mutually_different )
assume that
A1: a,b,c is_a_triangle and
A2: not a,b,c are_mutually_different ; :: thesis: contradiction

now

per cases ( a = b or b = c or c = a ) by A2, ZFMISC_1:def 5;

case A3: a = b ; :: thesis: contradiction

ex P being LINE of G st
( b on P & c on P ) by INCPROJ:def 5;
hence contradiction by A1, A3, Th5; :: thesis: verum

end;

case A4: b = c ; :: thesis: contradiction

ex P being LINE of G st
( a on P & b on P ) by INCPROJ:def 5;
hence contradiction by A1, A4, Th5; :: thesis: verum

end;

case A5: c = a ; :: thesis: contradiction

ex P being LINE of G st
( b on P & c on P ) by INCPROJ:def 5;
hence contradiction by A1, A5, Th5; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum