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

assume a = d ; :: thesis: contradiction
then a,b '||' c,a by A1, Def3;
then A3: a,b '||' a,c by PARSP_1:23;
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 PARSP_1:23;
then A5: a,b '||' a,c by PARSP_1:24;
not a,b,c is_collinear by A1, Def3;
hence contradiction by A5, Def2; :: thesis: verum

end;

A6: now

assume b = d ; :: thesis: contradiction
then a,b '||' c,b by A1, Def3;
then b,a '||' b,c by PARSP_1:23;
then A7: a,b '||' a,c by PARSP_1:24;
not a,b,c is_collinear by A1, Def3;
hence contradiction by A7, Def2; :: thesis: verum

end;

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