let FdSp be FanodesSp; for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
( not a,b,c are_collinear & not b,a,d are_collinear & not c,d,a are_collinear & not d,c,b are_collinear )
let a, b, c, d be Element of FdSp; ( parallelogram a,b,c,d implies ( not a,b,c are_collinear & not b,a,d are_collinear & not c,d,a are_collinear & not d,c,b are_collinear ) )
A1:
( a,b '||' b,a & a,c '||' c,a )
by PARSP_1:25;
assume A2:
parallelogram a,b,c,d
; ( not a,b,c are_collinear & not b,a,d are_collinear & not c,d,a are_collinear & not d,c,b are_collinear )
then A3:
d <> b
by Th26;
a,c '||' b,d
by A2;
then A4:
a,c '||' d,b
by PARSP_1:23;
a,b '||' c,d
by A2;
then A5:
a,b '||' d,c
by PARSP_1:23;
A6:
( not a,b,c are_collinear & d <> c )
by A2, Th26;
A7:
( a,b '||' c,d & c <> a )
by A2, Th26;
( a,c '||' b,d & b <> a )
by A2, Th26;
hence
( not a,b,c are_collinear & not b,a,d are_collinear & not c,d,a are_collinear & not d,c,b are_collinear )
by A1, A7, A5, A4, A6, A3, Th11; verum