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