theorem :: MSSCYC_2:3

for S being non empty void ManySortedSign holds
( S is monotonic iff InducedGraph S is well-founded )