let FdSp be FanodesSp; :: thesis: for a, b being Element of FdSp holds a,b congr a,b
let a, b be Element of FdSp; :: thesis: a,b congr a,b

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

assume a <> b ; :: thesis: a,b congr a,b
then consider p, q being Element of FdSp such that
A1: parallelogram a,b,p,q by Th43;
parallelogram p,q,a,b by A1, Th33;
hence a,b congr a,b ; :: thesis: verum

end;

hence a,b congr a,b ; :: thesis: verum