let SAS be Semi_Affine_Space; for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds
( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c )
let a, b, c, d be Element of SAS; ( parallelogram a,b,c,d implies ( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c ) )
assume A1:
parallelogram a,b,c,d
; ( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c )
then A2:
( not c,d,a is_collinear & not b,a,d is_collinear )
by Th56;
A3:
( not a,c,b is_collinear & a,c // b,d )
by A1, Def3, Th56;
A4:
( not c,a,d is_collinear & not d,b,c is_collinear )
by A1, Th56;
A5:
a,b // c,d
by A1, Def3;
then A6:
d,c // b,a
by Th17;
A7:
a,c // b,d
by A1, Def3;
then A8:
( c,a // d,b & b,d // a,c )
by Th17;
A9:
not b,d,a is_collinear
by A1, Th56;
A10:
d,b // c,a
by A7, Th17;
( c,d // a,b & b,a // d,c )
by A5, Th17;
hence
( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c )
by A5, A3, A2, A8, A4, A10, A6, A9, Def3; verum