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 is_collinear by Th20;
not b,a,d is_collinear by A1, Th15;
then consider c being Element of FdSp such that
A2: parallelogram b,a,d,c by Th42;
parallelogram a,b,c,d by A2, Th41;
hence ex b, c being Element of FdSp st parallelogram a,b,c,d ; :: thesis: verum