for FdSp being FanodesSp
for a, b being Element of FdSp holds a,b congr a,b