let SAS be Semi_Affine_Space; :: thesis: 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; :: thesis: ( a <> d implies ex b, c being Element of SAS st parallelogram a,b,c,d )
assume a <> d ; :: thesis: 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 ; :: thesis: verum