let G3 be _Graph; :: thesis: for v1, e being object
for v2 being Vertex of G3
for G2 being addVertex of G3,v1
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G3 & not v1 in the_Vertices_of G3 holds
G1 is addAdjVertex of G3,v1,e,v2
let v1, e be object ; :: thesis: for v2 being Vertex of G3
for G2 being addVertex of G3,v1
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G3 & not v1 in the_Vertices_of G3 holds
G1 is addAdjVertex of G3,v1,e,v2
let v2 be Vertex of G3; :: thesis: for G2 being addVertex of G3,v1
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G3 & not v1 in the_Vertices_of G3 holds
G1 is addAdjVertex of G3,v1,e,v2
let G2 be addVertex of G3,v1; :: thesis: for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G3 & not v1 in the_Vertices_of G3 holds
G1 is addAdjVertex of G3,v1,e,v2
let G1 be addEdge of G2,v1,e,v2; :: thesis: ( not e in the_Edges_of G3 & not v1 in the_Vertices_of G3 implies G1 is addAdjVertex of G3,v1,e,v2 )
assume A1: ( not e in the_Edges_of G3 & not v1 in the_Vertices_of G3 ) ; :: thesis: G1 is addAdjVertex of G3,v1,e,v2
A2: G1 is Supergraph of G3 by Th66;
A3: ( the_Vertices_of G2 = (the_Vertices_of G3) \/ {v1} & the_Edges_of G2 = the_Edges_of G3 & the_Source_of G2 = the_Source_of G3 & the_Target_of G2 = the_Target_of G3 ) by Def10;
A5: v2 is Vertex of G2 by Th72;
v1 is Vertex of G2 by Th98;
then ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ {e} & the_Source_of G1 = (the_Source_of G2) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G2) +* (e .--> v2) ) by A1, A3, A5, Def11;
hence G1 is addAdjVertex of G3,v1,e,v2 by A1, A2, A3, Def14; :: thesis: verum