theorem :: PARSP_2:47
for FdSp being FanodesSp
for a, b being Element of FdSp st a,b congr b,a holds
a = b by Th37;