let FdSp be FanodesSp; :: thesis: for a, b, c being Element of FdSp st not a,b,c are_collinear holds
ex d being Element of FdSp st parallelogram a,b,c,d
let a, b, c be Element of FdSp; :: thesis: ( not a,b,c are_collinear implies ex d being Element of FdSp st parallelogram a,b,c,d )
consider d being Element of FdSp such that
A1: ( a,b '||' c,d & a,c '||' b,d ) by PARSP_1:def 12;
assume not a,b,c are_collinear ; :: thesis: ex d being Element of FdSp st parallelogram a,b,c,d
then parallelogram a,b,c,d by A1;
hence ex d being Element of FdSp st parallelogram a,b,c,d ; :: thesis: verum