let S be non empty non void ManySortedSign ; :: thesis: ( S is monotonic implies InducedGraph S is well-founded )
set G = InducedGraph S;
assume S is monotonic ; :: thesis: InducedGraph S is well-founded
then reconsider S = S as non empty non void monotonic ManySortedSign ;
set A = the non-empty finite-yielding MSAlgebra over S;
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;
reconsider v = v as SortSymbol of S ;
consider s being non empty finite Subset of NAT such that
A2: s = { (depth t) where t is Element of the Sorts of (FreeEnv the non-empty finite-yielding MSAlgebra over S) . v : verum } and
depth (v, the non-empty finite-yielding MSAlgebra over S) = max s by CIRCUIT1:def 6;
max s is Nat by TARSKI:1;
then consider c being directed Chain of InducedGraph S such that
not c is empty and
A3: (vertex-seq c) . ((len c) + 1) = v and
A4: len c > max s by A1;
1 <= len c by A4, NAT_1:14;
then consider t being Element of the Sorts of (FreeMSA the Sorts of the non-empty finite-yielding MSAlgebra over S) . v such that
A5: depth t = len c by A3, Th2;
reconsider t9 = t as Element of the Sorts of (FreeEnv the non-empty finite-yielding MSAlgebra over S) . v ;
( ex t99 being Element of the Sorts of (FreeMSA the Sorts of the non-empty finite-yielding MSAlgebra over S) . v st
( t9 = t99 & depth t9 = depth t99 ) & depth t9 in s ) by A2, CIRCUIT1:def 5;
hence contradiction by A4, A5, XXREAL_2:def 8; :: thesis: verum