let FdSp be FanodesSp; :: thesis: for a, b, c, d being Element of FdSp st a,b congr c,d holds
b,a congr d,c
let a, b, c, d be Element of FdSp; :: thesis: ( a,b congr c,d implies b,a congr d,c )
assume A1: a,b congr c,d ; :: thesis: b,a congr d,c

A2: now :: thesis: ( a <> b implies b,a congr d,c )

assume a <> b ; :: thesis: b,a congr d,c
then consider p, q being Element of FdSp such that
A3: ( parallelogram p,q,a,b & parallelogram p,q,c,d ) by A1;
( parallelogram q,p,b,a & parallelogram q,p,d,c ) by A3, Th33;
hence b,a congr d,c ; :: thesis: verum

end;

( a = b implies b,a congr d,c ) by A1, Th45;
hence b,a congr d,c by A2; :: thesis: verum