let FdSp be FanodesSp; :: thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
( a <> b & b <> c & c <> a & a <> d & b <> d & c <> d )
let a, b, c, d be Element of FdSp; :: thesis: ( parallelogram a,b,c,d implies ( a <> b & b <> c & c <> a & a <> d & b <> d & c <> d ) )
assume A1: parallelogram a,b,c,d ; :: thesis: ( a <> b & b <> c & c <> a & 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 PARSP_1:23;
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 PARSP_1:23;
then A5: a,b '||' a,c by PARSP_1:24;
not a,b,c are_collinear by A1;
hence contradiction by A5; :: 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 PARSP_1:23;
then A7: a,b '||' a,c by PARSP_1:24;
not a,b,c are_collinear by A1;
hence contradiction by A7; :: thesis: verum

end;

not a,b,c are_collinear by A1;
hence ( a <> b & b <> c & c <> a & a <> d & b <> d & c <> d ) by A2, A6, A4, Th12; :: thesis: verum