let SAS be Semi_Affine_Space; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ( not a,b,c is_collinear & a,b // c,d & a,c // b,d ) by Def3;
then ( not a,c,b is_collinear & a,c // b,d & a,b // c,d & not c,d,a is_collinear & c,d // a,b & c,a // d,b & not b,a,d is_collinear & b,a // d,c & b,d // a,c & not c,a,d is_collinear & c,a // d,b & c,d // a,b & not d,b,c is_collinear & d,b // c,a & d,c // b,a & not b,d,a is_collinear & b,d // a,c & b,a // d,c ) by A1, Th17, Th56;
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 Def3; :: thesis: verum