let FdSp be FanodesSp; 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; ( 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
; 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
; verum