let FdSp be FanodesSp; :: thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
not parallelogram a,b,d,c
let a, b, c, d be Element of FdSp; :: thesis: ( parallelogram a,b,c,d implies not parallelogram a,b,d,c )
assume parallelogram a,b,c,d ; :: thesis: not parallelogram a,b,d,c
then not a,d '||' b,c by Th44;
hence not parallelogram a,b,d,c by Def3; :: thesis: verum