let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V
for x, y, e being object holds
( e Joins x,y,G1 iff e Joins x,y,G2 )
let V be set ; :: thesis: for G1 being addVertices of G2,V
for x, y, e being object holds
( e Joins x,y,G1 iff e Joins x,y,G2 )
let G1 be addVertices of G2,V; :: thesis: for x, y, e being object holds
( e Joins x,y,G1 iff e Joins x,y,G2 )
let x, y, e be object ; :: thesis: ( e Joins x,y,G1 iff e Joins x,y,G2 )
( e Joins x,y,G1 iff ( e DJoins x,y,G1 or e DJoins y,x,G1 ) ) by GLIB_000:16;
then ( e Joins x,y,G1 iff ( e DJoins x,y,G2 or e DJoins y,x,G2 ) ) by Th89;
hence ( e Joins x,y,G1 iff e Joins x,y,G2 ) by GLIB_000:16; :: thesis: verum