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 G' = 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 G' such that
A3: ( not dc is empty & 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:27;
then reconsider v = (vertex-seq dc) . 1 as Element of the carrier of G by FINSEQ_2:13;
consider n being Element of NAT such that
A4: for c being directed Chain of G' 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 G' such that
A5: ( len ch = n + 1 & ch ^ dc is non empty directed Chain of G' ) by A3, Th18;
reconsider ch = ch as non empty directed Chain of G' by A5;
reconsider cc = ch ^ dc as non empty directed Chain of G' by A5;
(vertex-seq dc) . 1 = (vertex-seq dc) . ((len dc) + 1) by A3, Th17;
then (vertex-seq cc) . ((len cc) + 1) = v by A3, Th16;
then A6: len cc <= n by A4;
len cc = (n + 1) + (len dc) by A5, FINSEQ_1:35;
then n + 1 <= len cc by NAT_1:11;
hence contradiction by A6, NAT_1:13; :: thesis: verum

end;

end;