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

now

assume a <> b ; :: thesis: contradiction
then ex p, q being Element of FdSp st
( parallelogram p,q,a,b & parallelogram p,q,b,a ) by A1, Def4;
hence contradiction by Th45; :: thesis: verum

end;

hence a = b ; :: thesis: verum