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 v2 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
v2 is Vertex of G1
let v1 be Vertex of G2; :: thesis: for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
v2 is Vertex of G1
let e, v2 be object ; :: thesis: for G1 being addAdjVertex of G2,v1,e,v2 st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
v2 is Vertex of G1
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis: ( not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 implies v2 is Vertex of G1 )
assume ( not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: v2 is Vertex of G1
then A1: the_Vertices_of G1 = (the_Vertices_of G2) \/ {v2} by Def13;
v2 in {v2} by TARSKI:def 1;
hence v2 is Vertex of G1 by A1, XBOOLE_0:def 3; :: thesis: verum