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