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_distinct

let a, b, c be POINT of G; :: thesis: ( a,b,c is_a_triangle implies a,b,c are_mutually_distinct )

assume that

A1: a,b,c is_a_triangle and

A2: not a,b,c are_mutually_distinct ; :: thesis: contradiction

a,b,c are_mutually_distinct

let a, b, c be POINT of G; :: thesis: ( a,b,c is_a_triangle implies a,b,c are_mutually_distinct )

assume that

A1: a,b,c is_a_triangle and

A2: not a,b,c are_mutually_distinct ; :: thesis: contradiction

now :: thesis: ( ( a = b & contradiction ) or ( b = c & contradiction ) or ( c = a & contradiction ) )end;

hence
contradiction
; :: thesis: verumper cases
( a = b or b = c or c = a )
by A2, ZFMISC_1:def 5;

end;

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;( b on P & c on P ) by INCPROJ:def 5;

hence contradiction by A1, A3, Th5; :: thesis: verum

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;( a on P & b on P ) by INCPROJ:def 5;

hence contradiction by A1, A4, Th5; :: thesis: verum

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;( b on P & c on P ) by INCPROJ:def 5;

hence contradiction by A1, A5, Th5; :: thesis: verum