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