let G1 be _Graph; :: thesis:
let G3 be Subgraph of G1; :: thesis:
let v, e, w be object ; :: thesis:
let G2 be addEdge of G3,v,e,w; :: thesis:
assume A1: e DJoins v,w,G1 ; :: thesis:

suppose A2: ( v in the_Vertices_of G3 & w in the_Vertices_of G3 & not e in the_Edges_of G3 ) ; :: thesis:

the_Vertices_of G2 = the_Vertices_of G3 by A2, GLIB_006:def 11;
hence the_Vertices_of G2 c= the_Vertices_of G1 ; :: thesis:
A3: {e} c= the_Edges_of G1 by A1, GLIB_000:def 14, ZFMISC_1:31;
A4: (the_Edges_of G3) \/ {e} c= the_Edges_of G1 by A3, XBOOLE_1:8;
A5: the_Edges_of G2 = (the_Edges_of G3) \/ {e} by A2, GLIB_006:def 11;
hence the_Edges_of G2 c= the_Edges_of G1 by A4; :: thesis:
let e0 be set ; :: thesis:
assume e0 in the_Edges_of G2 ; :: thesis:

per cases by A5, ZFMISC_1:136;

suppose A6: e0 in the_Edges_of G3 ; :: thesis:

hence (the_Source_of G2) . e0 = (the_Source_of G3) . e0 by GLIB_006:def 9
.= (the_Source_of G1) . e0 by A6, GLIB_000:def 32 ;
:: thesis:
thus (the_Target_of G2) . e0 = (the_Target_of G3) . e0 by A6, GLIB_006:def 9
.= (the_Target_of G1) . e0 by A6, GLIB_000:def 32 ; :: thesis:

end;

suppose A7: e0 = e ; :: thesis:

A8: e DJoins v,w,G2 by A2, GLIB_006:105;
hence (the_Source_of G2) . e0 = v by A7, GLIB_000:def 14
.= (the_Source_of G1) . e0 by A1, A7, GLIB_000:def 14 ;
:: thesis:
thus (the_Target_of G2) . e0 = w by A7, A8, GLIB_000:def 14
.= (the_Target_of G1) . e0 by A1, A7, GLIB_000:def 14 ; :: thesis:

end;

end;

end;

hence G2 is Subgraph of G1 by GLIB_000:def 32; :: thesis:

end;

suppose ( not v in the_Vertices_of G3 or not w in the_Vertices_of G3 or e in the_Edges_of G3 ) ; :: thesis:

then G2 == G3 by GLIB_006:def 11;
hence G2 is Subgraph of G1 by GLIB_000:92; :: thesis:

end;

end;