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 3 :: thesis: ( not c is empty implies not c is cyclic )
assume A2: not c is empty ; :: thesis: not c is cyclic
c is FinSequence of the carrier' of G by Def1;
hence not c is cyclic by A1, A2; :: thesis: verum