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 )
then A2: not a,b,c is_collinear by Def3;

A3: now

assume a = d ; :: thesis: contradiction
then a,b '||' c,a by A1, Def3;
then ( a,b '||' a,c & not a,b,c is_collinear ) by A1, Def3, PARSP_1:40;
hence contradiction by Def2; :: thesis: verum

end;

A4: now

assume b = d ; :: thesis: contradiction
then a,b '||' c,b by A1, Def3;
then b,a '||' b,c by PARSP_1:40;
then ( a,b '||' a,c & not a,b,c is_collinear ) by A1, Def3, PARSP_1:41;
hence contradiction by Def2; :: thesis: verum

end;

now

assume c = d ; :: thesis: contradiction
then a,c '||' b,c by A1, Def3;
then c,a '||' c,b by PARSP_1:40;
then ( a,b '||' a,c & not a,b,c is_collinear ) by A1, Def3, PARSP_1:41;
hence contradiction by Def2; :: thesis: verum

end;

hence ( a <> b & b <> c & c <> a & a <> d & b <> d & c <> d ) by A2, A3, A4, Th18; :: thesis: verum