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

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 Th51;
parallelogram p,q,a,b by A1, Th41;
hence a,b congr a,b by Def4; :: thesis: verum

end;

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