let G1 be reverseEdgeDirections of G,E; :: thesis: G1 is acyclic
for W1 being Walk of G1 holds not W1 is Cycle-like

proof

given W1 being Walk of G1 such that A1: W1 is Cycle-like ; :: thesis: contradiction
reconsider W = W1 as Walk of G by Th15;
W is Cycle-like by A1, GLIB_006:24;
hence contradiction by GLIB_002:def 2; :: thesis: verum

end;

hence G1 is acyclic by GLIB_002:def 2; :: thesis: verum