let G1 be _Graph; :: thesis: for G2 being reverseEdgeDirections of G1 st G1 is Dcomplete holds
G2 is Dcomplete
let G2 be reverseEdgeDirections of G1; :: thesis: ( G1 is Dcomplete implies G2 is Dcomplete )
assume A1: G1 is Dcomplete ; :: thesis: G2 is Dcomplete
let v, w be Vertex of G2; :: according to GLIB_016:def 1 :: thesis: ( v <> w implies ex e being object st e DJoins v,w,G2 )
A2: ( v is Vertex of G1 & w is Vertex of G1 ) by GLIB_007:4;
assume v <> w ; :: thesis: ex e being object st e DJoins v,w,G2
then consider e being object such that
A3: e DJoins w,v,G1 by A1, A2;
take e ; :: thesis: e DJoins v,w,G2
e in the_Edges_of G1 by A3, GLIB_000:def 14;
hence e DJoins v,w,G2 by A3, GLIB_007:7; :: thesis: verum