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