let G1 be _Graph; :: thesis: for G2 being reverseEdgeDirections of G1 holds
( G1 is Dcomplete iff G2 is Dcomplete )
let G2 be reverseEdgeDirections of G1; :: thesis: ( G1 is Dcomplete iff G2 is Dcomplete )
thus ( G1 is Dcomplete implies G2 is Dcomplete ) by Lm1; :: thesis: ( G2 is Dcomplete implies G1 is Dcomplete )
G1 is reverseEdgeDirections of G2, the_Edges_of G1 by GLIB_007:3;
then G1 is reverseEdgeDirections of G2 by GLIB_007:4;
hence ( G2 is Dcomplete implies G1 is Dcomplete ) by Lm1; :: thesis: verum