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