let FdSp be FanodesSp; :: thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear )
let a, b, c, d be Element of FdSp; :: thesis: ( parallelogram a,b,c,d implies ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear ) )
assume A1: parallelogram a,b,c,d ; :: thesis: ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear )
then A2: ( not a,b,c is_collinear & a,b '||' b,a & a,c '||' b,d & b <> a & b <> d ) by Def3, Th34, PARSP_1:42;
A3: ( not a,b,c is_collinear & a,b '||' c,d & a,c '||' c,a & c <> d & c <> a ) by A1, Def3, Th34, PARSP_1:42;
( a,b '||' c,d & a,c '||' b,d ) by A1, Def3;
then ( not a,b,c is_collinear & a,b '||' d,c & a,c '||' d,b & d <> c & d <> b ) by A1, Def3, Th34, PARSP_1:40;
hence ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear ) by A2, A3, Th17; :: thesis: verum