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 ;
consider A being non-empty finite-yielding MSAlgebra of 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 Element of 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 5;
reconsider v = v as SortSymbol of ;
consider s being non empty finite Subset of such that
A2: s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum } and
depth v,A = max s by CIRCUIT1:def 6;
max s in NAT by ORDINAL1:def 13;
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 A) . v such that
A5: depth t = len c by A3, Th2;
reconsider t' = t as Element of the Sorts of (FreeEnv A) . v ;
( ex t'' being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( t' = t'' & depth t' = depth t'' ) & depth t' in s ) by A2, CIRCUIT1:def 5;
hence contradiction by A4, A5, XXREAL_2:def 8; :: thesis: verum