assume 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
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;
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 (InducedGraph S) by MSSCYC_1:def 1;
then A3: rng e c= the carrier' of (InducedGraph S) by FINSEQ_1:def 4;
1 in dom e by A2, FINSEQ_5:6;
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 A3, Def1;
hence contradiction ; :: thesis: verum