theorem :: PARSP_2:46

for FdSp being FanodesSp
for a, b, c being Element of FdSp st a,b congr c,c holds
a = b by Th26;