let SAS be Semi_Affine_Space; for a, d being Element of SAS st a <> d holds
ex b, c being Element of SAS st parallelogram a,b,c,d
let a, d be Element of SAS; ( a <> d implies ex b, c being Element of SAS st parallelogram a,b,c,d )
assume
a <> d
; ex b, c being Element of SAS st parallelogram a,b,c,d
then consider b being Element of SAS such that
A1:
not a,d,b are_collinear
by Th25;
not b,a,d are_collinear
by A1, Th22;
then consider c being Element of SAS such that
A2:
parallelogram b,a,d,c
by Th44;
parallelogram a,b,c,d
by A2, Th43;
hence
ex b, c being Element of SAS st parallelogram a,b,c,d
; verum