let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d being Element of SAS 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 SAS; :: 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 ) )
A1: a,b // b,a by Def1;
assume A2: 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 )
hence not a,b,c is_collinear by Def3; :: thesis: ( not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear )
A3: ( b <> a & b <> d ) by A2, Th54;
a,c // b,d by A2, Def3;
then A4: a,c // d,b by Th17;
a,b // c,d by A2, Def3;
then A5: a,b // d,c by Th17;
( not a,b,c is_collinear & a,c // b,d ) by A2, Def3;
hence not b,a,d is_collinear by A1, A3, Th39; :: thesis: ( not c,d,a is_collinear & not d,c,b is_collinear )
A6: a,c // c,a by Def1;
A7: ( c <> d & c <> a ) by A2, Th54;
( not a,b,c is_collinear & a,b // c,d ) by A2, Def3;
hence not c,d,a is_collinear by A6, A7, Th39; :: thesis: not d,c,b is_collinear
A8: d <> b by A2, Th54;
( not a,b,c is_collinear & c <> d ) by A2, Def3, Th54;
hence not d,c,b is_collinear by A5, A4, A8, Th39; :: thesis: verum