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