let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds
( a <> b & a <> c & c <> b & a <> d & b <> d & c <> d )
let a, b, c, d be Element of SAS; :: thesis: ( parallelogram a,b,c,d implies ( a <> b & a <> c & c <> b & a <> d & b <> d & c <> d ) )
assume A1: parallelogram a,b,c,d ; :: thesis: ( a <> b & a <> c & c <> b & a <> d & b <> d & c <> d )
then not a,b,c are_collinear ;
hence ( a <> b & a <> c & c <> b ) by Th24; :: thesis: ( a <> d & b <> d & c <> d )
A2: now :: thesis: not a = d
assume a = d ; :: thesis: contradiction
then a,b // c,a by A1;
then A3: a,b // a,c by Th6;
not a,b,c are_collinear by A1;
hence contradiction by A3; :: thesis: verum
end;
A4: now :: thesis: not c = d
assume c = d ; :: thesis: contradiction
then a,c // b,c by A1;
then c,a // c,b by Th6;
then A5: c,a,b are_collinear ;
not a,b,c are_collinear by A1;
hence contradiction by A5, Th22; :: thesis: verum
end;
A6: now :: thesis: not b = d
assume b = d ; :: thesis: contradiction
then a,b // c,b by A1;
then b,a // b,c by Th6;
then A7: b,a,c are_collinear ;
not a,b,c are_collinear by A1;
hence contradiction by A7, Th22; :: thesis: verum
end;
assume ( not a <> d or not b <> d or not c <> d ) ; :: thesis: contradiction
hence contradiction by A2, A6, A4; :: thesis: verum