let G1 be reverseEdgeDirections of G,E; :: thesis: not G1 is acyclic
reconsider G2 = G as reverseEdgeDirections of G1,E by Th3;
assume G1 is acyclic ; :: thesis: contradiction
then G2 is acyclic ;
hence contradiction ; :: thesis: verum