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

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 ) )

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

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;

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;

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;

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;

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;

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;

end;

end;

hence contradiction ; :: thesis: verum