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 is_collinear by Th41;
not b,a,d is_collinear by A1, Th37;
then consider c being Element of SAS such that
A2: parallelogram b,a,d,c by Th62;
parallelogram a,b,c,d by A2, Th61;
hence ex b, c being Element of SAS st parallelogram a,b,c,d ; :: thesis: verum