let G1 be reverseEdgeDirections of G; :: thesis: not G1 is non-Dmulti
reconsider G2 = G as reverseEdgeDirections of G1 by Th5;
assume G1 is non-Dmulti ; :: thesis: contradiction
then G2 is non-Dmulti ;
hence contradiction ; :: thesis: verum