let G be Graph; :: thesis: ( G is void implies G is well-founded )
assume G is void ; :: thesis: G is well-founded
then reconsider G9 = G as void Graph ;
let v be Element of the carrier of G; :: according to MSSCYC_1:def 4 :: thesis: ex n being Nat st
for c being directed Chain of G st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds
len c <= n
take 0 ; :: thesis: for c being directed Chain of G st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds
len c <= 0
let c be directed Chain of G; :: thesis: ( not c is empty & (vertex-seq c) . ((len c) + 1) = v implies len c <= 0 )
reconsider c = c as Chain of G9 ;
c is empty ;
hence ( not c is empty & (vertex-seq c) . ((len c) + 1) = v implies len c <= 0 ) ; :: thesis: verum