let G2 be _Graph; :: thesis: for v being object
for G1 being addAdjVertexAll of G2,v, {} holds G1 is addVertex of G2,v
let v be object ; :: thesis: for G1 being addAdjVertexAll of G2,v, {} holds G1 is addVertex of G2,v
let G1 be addAdjVertexAll of G2,v, {} ; :: thesis: G1 is addVertex of G2,v

per cases ( ( {} c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) or not {} c= the_Vertices_of G2 or v in the_Vertices_of G2 ) ;

suppose ( {} c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: G1 is addVertex of G2,v

then A1: the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by Def4;
A2: the_Edges_of G1 = the_Edges_of G2 by Th46;
then A3: ( dom (the_Source_of G1) = the_Edges_of G2 & dom (the_Target_of G1) = the_Edges_of G2 ) by GLIB_000:4;
A4: the_Source_of G1 = (the_Source_of G1) | (the_Edges_of G2) by A3
.= the_Source_of G2 by GLIB_006:69 ;
the_Target_of G1 = (the_Target_of G1) | (the_Edges_of G2) by A3
.= the_Target_of G2 by GLIB_006:69 ;
hence G1 is addVertex of G2,v by A1, A2, A4, GLIB_006:def 10; :: thesis: verum

end;

suppose A5: ( not {} c= the_Vertices_of G2 or v in the_Vertices_of G2 ) ; :: thesis: G1 is addVertex of G2,v

then A6: {v} c= the_Vertices_of G2 by XBOOLE_1:2, ZFMISC_1:31;
G1 == G2 by A5, Def4;
hence G1 is addVertex of G2,v by A6, GLIB_006:79; :: thesis: verum

end;

end;