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