let S be non empty non void ManySortedSign ; :: thesis: ( S is finitely_operated & InducedGraph S is well-founded implies S is monotonic )
set G = InducedGraph S;
assume A1: ( S is finitely_operated & InducedGraph S is well-founded ) ; :: thesis: S is monotonic
given A being non-empty finitely-generated MSAlgebra of S such that A2: not A is finite-yielding ; :: according to MSAFREE2:def 13 :: thesis: contradiction
consider GS being V2() V29() GeneratorSet of A;
reconsider gs = GS as V2() V29() ManySortedSet of ;
not FreeMSA gs is finite-yielding by A2, MSSCYC_1:23;
then not the Sorts of (FreeMSA gs) is finite-yielding by MSAFREE2:def 11;
then consider v being set such that
A3: ( v in the carrier of S & not the Sorts of (FreeMSA gs) . v is finite ) by FINSET_1:def 4;
reconsider v = v as SortSymbol of S by A3;
consider n being Element of NAT such that
A4: for c being directed Chain of InducedGraph S st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds
len c <= n by A1, MSSCYC_1:def 5;
set V = the Sorts of (FreeMSA gs) . v;
set Vn = { t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } ;
A5: { t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } is finite by A1, Th5;
not the Sorts of (FreeMSA gs) . v c= { t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } by A3, A5;
then consider t being set such that
A6: ( t in the Sorts of (FreeMSA gs) . v & not t in { t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } ) by TARSKI:def 3;
reconsider t = t as Element of the Sorts of (FreeMSA gs) . v by A6;
A7: not depth t <= n by A6;
then 1 <= depth t by NAT_1:14;
then consider d being directed Chain of InducedGraph S such that
A8: ( len d = depth t & (vertex-seq d) . ((len d) + 1) = v ) by Th2;
not d is empty by A7, A8, CARD_1:47;
hence contradiction by A4, A7, A8; :: thesis: verum