let S be non empty void ManySortedSign ; :: thesis: ( S is monotonic iff InducedGraph S is well-founded )
set G = InducedGraph S;
set OS = the carrier' of S;
set CA = the carrier of S;
set AR = the Arity of S;
hereby :: thesis: ( InducedGraph S is well-founded implies S is monotonic )
assume S is monotonic ; :: thesis:
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;
consider e being directed Chain of InducedGraph S such that
A2: not e is empty and
(vertex-seq e) . ((len e) + 1) = v and
len e > 0 by A1;
e is FinSequence of the carrier' of () by MSSCYC_1:def 1;
then A3: rng e c= the carrier' of () by FINSEQ_1:def 4;
1 in dom e by ;
then e . 1 in rng e by FUNCT_1:def 3;
then ex op, v being set st
( e . 1 = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) by ;
hence contradiction ; :: thesis: verum
end;
assume InducedGraph S is well-founded ; :: thesis: S is monotonic
let A be non-empty finitely-generated MSAlgebra over S; :: according to MSAFREE2:def 13 :: thesis:
thus the Sorts of A is V39() by MSAFREE2:def 10; :: according to MSAFREE2:def 11 :: thesis: verum