let G2 be _Graph; :: thesis: for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 holds
ex G3 being addVertex of G2,v2 st G1 is addEdge of G3,v1,e,v2
let v1 be Vertex of G2; :: thesis: for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 holds
ex G3 being addVertex of G2,v2 st G1 is addEdge of G3,v1,e,v2
let e, v2 be object ; :: thesis: for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 holds
ex G3 being addVertex of G2,v2 st G1 is addEdge of G3,v1,e,v2
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis: ( not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 implies ex G3 being addVertex of G2,v2 st G1 is addEdge of G3,v1,e,v2 )
assume A1: ( not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 ) ; :: thesis: ex G3 being addVertex of G2,v2 st G1 is addEdge of G3,v1,e,v2
set G3 = the addVertex of G2,v2;
take the addVertex of G2,v2 ; :: thesis: G1 is addEdge of the addVertex of G2,v2,v1,e,v2
A2: ( the_Vertices_of G1 = (the_Vertices_of G2) \/ {v2} & 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, Def13;
A3: ( the_Vertices_of the addVertex of G2,v2 = (the_Vertices_of G2) \/ {v2} & the_Edges_of the addVertex of G2,v2 = the_Edges_of G2 & the_Source_of the addVertex of G2,v2 = the_Source_of G2 & the_Target_of the addVertex of G2,v2 = the_Target_of G2 ) by Def10;
the_Vertices_of G2 c= the_Vertices_of the addVertex of G2,v2 by Def9;
then A5: v1 in the_Vertices_of the addVertex of G2,v2 by TARSKI:def 3;
A6: v2 is Vertex of the addVertex of G2,v2 by Th98;
A8: the_Edges_of the addVertex of G2,v2 c= the_Edges_of G1 by A2, A3, XBOOLE_1:11;
for e1 being set st e1 in the_Edges_of the addVertex of G2,v2 holds
( (the_Source_of the addVertex of G2,v2) . e1 = (the_Source_of G1) . e1 & (the_Target_of the addVertex of G2,v2) . e1 = (the_Target_of G1) . e1 ) by A3, Def9;
then G1 is Supergraph of the addVertex of G2,v2 by A2, A3, A8, Def9;
hence G1 is addEdge of the addVertex of G2,v2,v1,e,v2 by A1, A2, A3, A5, A6, Def11; :: thesis: verum