theorem :: PARSP_2:53

for FdSp being FanodesSp
for a, b, c, x, y being Element of FdSp st a,b congr c,x & a,b congr c,y holds
x = y