let G1, G2 be _Graph; :: thesis: ( G1 == G2 & G1 is Dcomplete implies G2 is Dcomplete )
assume A1: ( G1 == G2 & 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 A1, GLIB_000:def 34;
assume v <> w ; :: thesis: ex e being object st e DJoins v,w,G2
then consider e being object such that
A3: e DJoins v,w,G1 by A1, A2;
take e ; :: thesis: e DJoins v,w,G2
thus e DJoins v,w,G2 by A1, A3, GLIB_000:88; :: thesis: verum