let G be IncProjSp; :: thesis: for a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle holds

a,b,c,d are_mutually_distinct

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

assume that

A1: a,b,c,d is_a_quadrangle and

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

a,b,c,d are_mutually_distinct

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

assume that

A1: a,b,c,d is_a_quadrangle and

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

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

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

end;

case
a = b
; :: thesis: contradiction

then
not a,b,c are_mutually_distinct
by ZFMISC_1:def 5;

then not a,b,c is_a_triangle by Th26;

hence contradiction by A1; :: thesis: verum

end;then not a,b,c is_a_triangle by Th26;

hence contradiction by A1; :: thesis: verum

case
b = c
; :: thesis: contradiction

then
not a,b,c are_mutually_distinct
by ZFMISC_1:def 5;

then not a,b,c is_a_triangle by Th26;

hence contradiction by A1; :: thesis: verum

end;then not a,b,c is_a_triangle by Th26;

hence contradiction by A1; :: thesis: verum

case
c = a
; :: thesis: contradiction

then
not a,b,c are_mutually_distinct
by ZFMISC_1:def 5;

then not a,b,c is_a_triangle by Th26;

hence contradiction by A1; :: thesis: verum

end;then not a,b,c is_a_triangle by Th26;

hence contradiction by A1; :: thesis: verum

case
d = a
; :: thesis: contradiction

then
not d,a,b are_mutually_distinct
by ZFMISC_1:def 5;

then not d,a,b is_a_triangle by Th26;

hence contradiction by A1; :: thesis: verum

end;then not d,a,b is_a_triangle by Th26;

hence contradiction by A1; :: thesis: verum

case
d = b
; :: thesis: contradiction

then
not d,a,b are_mutually_distinct
by ZFMISC_1:def 5;

then not d,a,b is_a_triangle by Th26;

hence contradiction by A1; :: thesis: verum

end;then not d,a,b is_a_triangle by Th26;

hence contradiction by A1; :: thesis: verum

case
d = c
; :: thesis: contradiction

then
not b,c,d are_mutually_distinct
by ZFMISC_1:def 5;

then not b,c,d is_a_triangle by Th26;

hence contradiction by A1; :: thesis: verum

end;then not b,c,d is_a_triangle by Th26;

hence contradiction by A1; :: thesis: verum