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 ) )
assume A1: 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 )
( not a,b,c is_collinear & a,b // b,a & a,c // b,d & b <> a & b <> d ) by A1, Def1, Def3, Th54;
hence not b,a,d is_collinear by Th39; :: thesis: ( not c,d,a is_collinear & not d,c,b is_collinear )
( not a,b,c is_collinear & a,b // c,d & a,c // c,a & c <> d & c <> a ) by A1, Def1, Def3, Th54;
hence not c,d,a is_collinear by Th39; :: thesis: not d,c,b is_collinear
( not a,b,c is_collinear & a,b // c,d & a,c // b,d & c <> d & d <> b ) by A1, Def3, Th54;
then ( not a,b,c is_collinear & a,b // d,c & a,c // d,b & c <> d & d <> b ) by Th17;
hence not d,c,b is_collinear by Th39; :: thesis: verum