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 is_collinear by Def3;
hence ( a <> b & a <> c & c <> b ) by Th40; :: thesis: ( a <> d & b <> d & c <> d )

A2: now

assume a = d ; :: thesis: contradiction
then a,b // c,a by A1, Def3;
then A3: a,b // a,c by Th17;
not a,b,c is_collinear by A1, Def3;
hence contradiction by A3, Def2; :: thesis: verum

end;

A4: now

assume c = d ; :: thesis: contradiction
then a,c // b,c by A1, Def3;
then c,a // c,b by Th17;
then A5: c,a,b is_collinear by Def2;
not a,b,c is_collinear by A1, Def3;
hence contradiction by A5, Th37; :: thesis: verum

end;

A6: now

assume b = d ; :: thesis: contradiction
then a,b // c,b by A1, Def3;
then b,a // b,c by Th17;
then A7: b,a,c is_collinear by Def2;
not a,b,c is_collinear by A1, Def3;
hence contradiction by A7, Th37; :: 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