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