let S be non empty void ManySortedSign ; :: thesis: ( S is monotonic iff InducedGraph S is well-founded )
set G = InducedGraph S;
set OS = the carrier' of S;
set CA = the carrier of S;
set AR = the Arity of S;

hereby :: thesis: ( InducedGraph S is well-founded implies S is monotonic )

assume S is monotonic ; :: thesis: InducedGraph S is well-founded
assume not InducedGraph S is well-founded ; :: thesis: contradiction
then consider v being Element of the carrier of (InducedGraph S) such that
A1: for n being Nat ex c being directed Chain of InducedGraph S st
( not c is empty & (vertex-seq c) . ((len c) + 1) = v & len c > n ) by MSSCYC_1:def 4;
consider e being directed Chain of InducedGraph S such that
A2: not e is empty and
(vertex-seq e) . ((len e) + 1) = v and
len e > 0 by A1;
e is FinSequence of the carrier' of (InducedGraph S) by MSSCYC_1:def 1;
then A3: rng e c= the carrier' of (InducedGraph S) by FINSEQ_1:def 4;
1 in dom e by A2, FINSEQ_5:6;
then e . 1 in rng e by FUNCT_1:def 3;
then ex op, v being set st
( e . 1 = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) by A3, Def1;
hence contradiction ; :: thesis: verum

end;

assume InducedGraph S is well-founded ; :: thesis: S is monotonic
let A be non-empty finitely-generated MSAlgebra over S; :: according to MSAFREE2:def 13 :: thesis: A is finite-yielding
thus the Sorts of A is finite-yielding by MSAFREE2:def 10; :: according to MSAFREE2:def 11 :: thesis: verum