let G be Graph; :: thesis: ( G is well-founded implies G is directed_cycle-less )

per cases ( G is void or not G is void ) ;

suppose G is void ; :: thesis: ( G is well-founded implies G is directed_cycle-less )

then reconsider G = G as void Graph ;
G is directed_cycle-less ;
hence ( G is well-founded implies G is directed_cycle-less ) ; :: thesis: verum

end;

suppose not G is void ; :: thesis: ( G is well-founded implies G is directed_cycle-less )

then reconsider G9 = G as non void Graph ;
assume that
A1: G is well-founded and
A2: not G is directed_cycle-less ; :: thesis: contradiction
consider dc being directed Chain of G9 such that
A3: not dc is empty and
A4: dc is cyclic by A2, Def4;
set p = vertex-seq dc;
len (vertex-seq dc) = (len dc) + 1 by A3, Th10;
then 1 <= len (vertex-seq dc) by NAT_1:11;
then 1 in dom (vertex-seq dc) by FINSEQ_3:25;
then reconsider v = (vertex-seq dc) . 1 as Element of the carrier of G by FINSEQ_2:11;
consider n being Element of NAT such that
A5: for c being directed Chain of G9 st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds
len c <= n by A1, Def5;
consider ch being directed Chain of G9 such that
A6: len ch = n + 1 and
A7: ch ^ dc is non empty directed Chain of G9 by A3, A4, Th18;
reconsider ch = ch as non empty directed Chain of G9 by A6;
reconsider cc = ch ^ dc as non empty directed Chain of G9 by A7;
(vertex-seq dc) . 1 = (vertex-seq dc) . ((len dc) + 1) by A3, A4, Th17;
then (vertex-seq cc) . ((len cc) + 1) = v by A3, Th16;
then A8: len cc <= n by A5;
len cc = (n + 1) + (len dc) by A6, FINSEQ_1:22;
then n + 1 <= len cc by NAT_1:11;
hence contradiction by A8, NAT_1:13; :: thesis: verum

end;

end;