:: deftheorem defines directed_cycle-less MSSCYC_1:def 3 :
for IT being Graph holds
( IT is directed_cycle-less iff for dc being directed Chain of IT st not dc is empty holds
not dc is cyclic );