let SAS be Semi_Affine_Space; for a1, a2, a3, a4 being Element of SAS st parallelogram a1,a2,a3,a4 holds
( not a1,a2,a3 is_collinear & not a1,a3,a2 is_collinear & not a1,a2,a4 is_collinear & not a1,a4,a2 is_collinear & not a1,a3,a4 is_collinear & not a1,a4,a3 is_collinear & not a2,a1,a3 is_collinear & not a2,a3,a1 is_collinear & not a2,a1,a4 is_collinear & not a2,a4,a1 is_collinear & not a2,a3,a4 is_collinear & not a2,a4,a3 is_collinear & not a3,a1,a2 is_collinear & not a3,a2,a1 is_collinear & not a3,a1,a4 is_collinear & not a3,a4,a1 is_collinear & not a3,a2,a4 is_collinear & not a3,a4,a2 is_collinear & not a4,a1,a2 is_collinear & not a4,a2,a1 is_collinear & not a4,a1,a3 is_collinear & not a4,a3,a1 is_collinear & not a4,a2,a3 is_collinear & not a4,a3,a2 is_collinear )
let a1, a2, a3, a4 be Element of SAS; ( parallelogram a1,a2,a3,a4 implies ( not a1,a2,a3 is_collinear & not a1,a3,a2 is_collinear & not a1,a2,a4 is_collinear & not a1,a4,a2 is_collinear & not a1,a3,a4 is_collinear & not a1,a4,a3 is_collinear & not a2,a1,a3 is_collinear & not a2,a3,a1 is_collinear & not a2,a1,a4 is_collinear & not a2,a4,a1 is_collinear & not a2,a3,a4 is_collinear & not a2,a4,a3 is_collinear & not a3,a1,a2 is_collinear & not a3,a2,a1 is_collinear & not a3,a1,a4 is_collinear & not a3,a4,a1 is_collinear & not a3,a2,a4 is_collinear & not a3,a4,a2 is_collinear & not a4,a1,a2 is_collinear & not a4,a2,a1 is_collinear & not a4,a1,a3 is_collinear & not a4,a3,a1 is_collinear & not a4,a2,a3 is_collinear & not a4,a3,a2 is_collinear ) )
assume A1:
parallelogram a1,a2,a3,a4
; ( not a1,a2,a3 is_collinear & not a1,a3,a2 is_collinear & not a1,a2,a4 is_collinear & not a1,a4,a2 is_collinear & not a1,a3,a4 is_collinear & not a1,a4,a3 is_collinear & not a2,a1,a3 is_collinear & not a2,a3,a1 is_collinear & not a2,a1,a4 is_collinear & not a2,a4,a1 is_collinear & not a2,a3,a4 is_collinear & not a2,a4,a3 is_collinear & not a3,a1,a2 is_collinear & not a3,a2,a1 is_collinear & not a3,a1,a4 is_collinear & not a3,a4,a1 is_collinear & not a3,a2,a4 is_collinear & not a3,a4,a2 is_collinear & not a4,a1,a2 is_collinear & not a4,a2,a1 is_collinear & not a4,a1,a3 is_collinear & not a4,a3,a1 is_collinear & not a4,a2,a3 is_collinear & not a4,a3,a2 is_collinear )
then A2:
( not a3,a4,a1 is_collinear & not a4,a3,a2 is_collinear )
by Th55;
( not a1,a2,a3 is_collinear & not a2,a1,a4 is_collinear )
by A1, Th55;
hence
( not a1,a2,a3 is_collinear & not a1,a3,a2 is_collinear & not a1,a2,a4 is_collinear & not a1,a4,a2 is_collinear & not a1,a3,a4 is_collinear & not a1,a4,a3 is_collinear & not a2,a1,a3 is_collinear & not a2,a3,a1 is_collinear & not a2,a1,a4 is_collinear & not a2,a4,a1 is_collinear & not a2,a3,a4 is_collinear & not a2,a4,a3 is_collinear & not a3,a1,a2 is_collinear & not a3,a2,a1 is_collinear & not a3,a1,a4 is_collinear & not a3,a4,a1 is_collinear & not a3,a2,a4 is_collinear & not a3,a4,a2 is_collinear & not a4,a1,a2 is_collinear & not a4,a2,a1 is_collinear & not a4,a1,a3 is_collinear & not a4,a3,a1 is_collinear & not a4,a2,a3 is_collinear & not a4,a3,a2 is_collinear )
by A2, Th37; verum