let G2 be _Graph; :: thesis: for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds
( the_Vertices_of G1 c= (the_Vertices_of G2) \/ {v,w} & the_Edges_of G1 c= (the_Edges_of G2) \/ {e} )
let v, e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w holds
( the_Vertices_of G1 c= (the_Vertices_of G2) \/ {v,w} & the_Edges_of G1 c= (the_Edges_of G2) \/ {e} )
let G1 be addAdjVertex of G2,v,e,w; :: thesis: ( the_Vertices_of G1 c= (the_Vertices_of G2) \/ {v,w} & the_Edges_of G1 c= (the_Edges_of G2) \/ {e} )

per cases ( ( v in the_Vertices_of G2 & not w in the_Vertices_of G2 & not e in the_Edges_of G2 ) or ( not v in the_Vertices_of G2 & w in the_Vertices_of G2 & not e in the_Edges_of G2 ) or ( not ( v in the_Vertices_of G2 & not w in the_Vertices_of G2 & not e in the_Edges_of G2 ) & not ( not v in the_Vertices_of G2 & w in the_Vertices_of G2 & not e in the_Edges_of G2 ) ) ) ;

suppose ( v in the_Vertices_of G2 & not w in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: ( the_Vertices_of G1 c= (the_Vertices_of G2) \/ {v,w} & the_Edges_of G1 c= (the_Edges_of G2) \/ {e} )

then ( the_Vertices_of G1 = (the_Vertices_of G2) \/ {w} & the_Edges_of G1 = (the_Edges_of G2) \/ {e} ) by GLIB_006:def 12;
hence ( the_Vertices_of G1 c= (the_Vertices_of G2) \/ {v,w} & the_Edges_of G1 c= (the_Edges_of G2) \/ {e} ) by ZFMISC_1:7, XBOOLE_1:9; :: thesis: verum

end;

suppose ( not v in the_Vertices_of G2 & w in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: ( the_Vertices_of G1 c= (the_Vertices_of G2) \/ {v,w} & the_Edges_of G1 c= (the_Edges_of G2) \/ {e} )

then ( the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} & the_Edges_of G1 = (the_Edges_of G2) \/ {e} ) by GLIB_006:def 12;
hence ( the_Vertices_of G1 c= (the_Vertices_of G2) \/ {v,w} & the_Edges_of G1 c= (the_Edges_of G2) \/ {e} ) by ZFMISC_1:7, XBOOLE_1:9; :: thesis: verum

end;

suppose ( not ( v in the_Vertices_of G2 & not w in the_Vertices_of G2 & not e in the_Edges_of G2 ) & not ( not v in the_Vertices_of G2 & w in the_Vertices_of G2 & not e in the_Edges_of G2 ) ) ; :: thesis: ( the_Vertices_of G1 c= (the_Vertices_of G2) \/ {v,w} & the_Edges_of G1 c= (the_Edges_of G2) \/ {e} )

then G1 == G2 by GLIB_006:def 12;
then ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by GLIB_000:def 34;
hence ( the_Vertices_of G1 c= (the_Vertices_of G2) \/ {v,w} & the_Edges_of G1 c= (the_Edges_of G2) \/ {e} ) by XBOOLE_1:7; :: thesis: verum

end;

end;