theorem Th20: :: NECKLA_3:20

for G being non empty irreflexive RelStr
for x being Element of G
for x9 being Element of (ComplRelStr G) st x = x9 holds
ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x9})