let FdSp be FanodesSp; :: thesis: for a, b, c being Element of FdSp st a,b congr c,c holds
a = b
let a, b, c be Element of FdSp; :: thesis: ( a,b congr c,c implies a = b )
assume a,b congr c,c ; :: thesis: a = b
then ( ( a = b & c = c ) or ex p, q being Element of FdSp st
( parallelogram p,q,a,b & parallelogram p,q,c,c ) ) by Def4;
hence a = b by Th34; :: thesis: verum