let G be Graph; :: thesis: ( G is void implies G is directed_cycle-less )
assume A1: G is void ; :: thesis: G is directed_cycle-less
let c be directed Chain of G; :: according to MSSCYC_1:def 4 :: thesis: ( not c is empty implies not c is cyclic )
assume not c is empty ; :: thesis: not c is cyclic
then 1 in dom c by FINSEQ_5:6;
then A2: c . 1 in rng c by FUNCT_1:def 5;
c is FinSequence of the carrier' of G by Def1;
then rng c c= the carrier' of G by FINSEQ_1:def 4;
hence not c is cyclic by A1, A2; :: thesis: verum