let SAS be Semi_Affine_Space; for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds
not parallelogram a,b,d,c
let a, b, c, d be Element of SAS; ( parallelogram a,b,c,d implies not parallelogram a,b,d,c )
assume A1:
parallelogram a,b,c,d
; not parallelogram a,b,d,c
then
not a,b,c are_collinear
;
then A2:
not a,b // a,c
;
assume
parallelogram a,b,d,c
; contradiction
then A3:
a,d // b,c
;
( a,b // c,d & a,c // b,d )
by A1;
hence
contradiction
by A3, A2, Def1; verum