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:
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 () such that
A1: for n being Nat ex c being directed Chain of InducedGraph S st
( not c is empty & () . ((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 = { () where t is Element of the Sorts of () . 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 ;
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 ;
reconsider t9 = t as Element of the Sorts of () . 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 ;
hence contradiction by A4, A5, XXREAL_2:def 8; :: thesis: verum