let SAS be Semi_Affine_Space; for a, b, c, d being Element of SAS 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 SAS; ( 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
by Def1;
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 )
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 )
A3:
( b <> a & b <> d )
by A2, Th36;
a,c // b,d
by A2;
then A4:
a,c // d,b
by Th6;
a,b // c,d
by A2;
then A5:
a,b // d,c
by Th6;
( not a,b,c are_collinear & a,c // b,d )
by A2;
hence
not b,a,d are_collinear
by A1, A3, Th23; ( not c,d,a are_collinear & not d,c,b are_collinear )
A6:
a,c // c,a
by Def1;
A7:
( c <> d & c <> a )
by A2, Th36;
( not a,b,c are_collinear & a,b // c,d )
by A2;
hence
not c,d,a are_collinear
by A6, A7, Th23; not d,c,b are_collinear
A8:
d <> b
by A2, Th36;
( not a,b,c are_collinear & c <> d )
by A2, Th36;
hence
not d,c,b are_collinear
by A5, A4, A8, Th23; verum