for S being non empty non void ManySortedSign st S is finitely_operated & InducedGraph S is well-founded holds
S is monotonic