let G, G2 be _Graph; :: thesis: for v1, e, v2 being object
for G1 being addAdjVertex of G,v1,e,v2 st G1 == G2 holds
G2 is addAdjVertex of G,v1,e,v2
let v1, e, v2 be object ; :: thesis: for G1 being addAdjVertex of G,v1,e,v2 st G1 == G2 holds
G2 is addAdjVertex of G,v1,e,v2
let G1 be addAdjVertex of G,v1,e,v2; :: thesis: ( G1 == G2 implies G2 is addAdjVertex of G,v1,e,v2 )
assume A1: G1 == G2 ; :: thesis: G2 is addAdjVertex of G,v1,e,v2

per cases ( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ) ) ;

suppose A2: ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis: G2 is addAdjVertex of G,v1,e,v2

then ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v2} & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) ) by Def12;
then A3: ( the_Vertices_of G2 = (the_Vertices_of G) \/ {v2} & the_Edges_of G2 = (the_Edges_of G) \/ {e} & the_Source_of G2 = (the_Source_of G) +* (e .--> v1) & the_Target_of G2 = (the_Target_of G) +* (e .--> v2) ) by A1, GLIB_000:def 34;
G2 is Supergraph of G1 by A1, Th62;
then G2 is Supergraph of G by Th66;
hence G2 is addAdjVertex of G,v1,e,v2 by A2, A3, Def12; :: thesis: verum

end;

suppose A4: ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis: G2 is addAdjVertex of G,v1,e,v2

then ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v1} & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) ) by Def12;
then A5: ( the_Vertices_of G2 = (the_Vertices_of G) \/ {v1} & the_Edges_of G2 = (the_Edges_of G) \/ {e} & the_Source_of G2 = (the_Source_of G) +* (e .--> v1) & the_Target_of G2 = (the_Target_of G) +* (e .--> v2) ) by A1, GLIB_000:def 34;
G2 is Supergraph of G1 by A1, Th62;
then G2 is Supergraph of G by Th66;
hence G2 is addAdjVertex of G,v1,e,v2 by A4, A5, Def12; :: thesis: verum

end;

suppose A6: ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ) ; :: thesis: G2 is addAdjVertex of G,v1,e,v2

then G == G1 by Def12;
then A7: G == G2 by A1, GLIB_000:85;
then G2 is Supergraph of G by Th62;
hence G2 is addAdjVertex of G,v1,e,v2 by A6, A7, Def12; :: thesis: verum

end;

end;