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

consider P being LINE of G such that
A4: ( b on P & c on P ) by INCPROJ:def 10;
thus contradiction by A1, A3, A4, Th5; :: thesis: verum

end;

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

consider P being LINE of G such that
A6: ( a on P & b on P ) by INCPROJ:def 10;
thus contradiction by A1, A5, A6, Th5; :: thesis: verum

end;

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

consider P being LINE of G such that
A8: ( b on P & c on P ) by INCPROJ:def 10;
thus contradiction by A1, A7, A8, Th5; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum