:: deftheorem defines well-founded MSSCYC_1:def 4 :
for IT being Graph holds
( IT is well-founded iff for v being Element of the carrier of IT ex n being Nat st
for c being directed Chain of IT st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds
len c <= n );