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