let SAS be Semi_Affine_Space; :: thesis: for a, b, c being Element of SAS st not a,b,c is_collinear holds
ex d being Element of SAS st parallelogram a,b,c,d
let a, b, c be Element of SAS; :: thesis: ( not a,b,c is_collinear implies ex d being Element of SAS st parallelogram a,b,c,d )
assume A1: not a,b,c is_collinear ; :: thesis: ex d being Element of SAS st parallelogram a,b,c,d
consider d being Element of SAS such that
A2: ( a,b // c,d & a,c // b,d ) by Def1;
take d ; :: thesis: parallelogram a,b,c,d
thus parallelogram a,b,c,d by A1, A2, Def3; :: thesis: verum