let G1 be addAdjVertexAll of G,v,V; :: thesis: G1 is non-Dmulti

per cases ( ( V c= the_Vertices_of G & not v in the_Vertices_of G ) or not V c= the_Vertices_of G or v in the_Vertices_of G ) ;

suppose A1: ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: G1 is non-Dmulti

for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 holds
e1 = e2

proof

let e1, e2, v1, v2 be object ; :: thesis: ( e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 implies e1 = e2 )
assume A2: ( e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 ) ; :: thesis: e1 = e2
then A3: ( e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 ) by GLIB_000:16;
consider E being set such that
( card V = card E & E misses the_Edges_of G & the_Edges_of G1 = (the_Edges_of G) \/ E ) and
A4: for v1 being object st v1 in V holds
ex e being object st
( e in E & e Joins v1,v,G1 & ( for e3 being object st e3 Joins v1,v,G1 holds
e = e3 ) ) by A1, Def4;

per cases ( ( v1 = v & v2 = v ) or ( v1 = v & v2 <> v ) or ( v1 <> v & v2 = v ) or ( v1 <> v & v2 <> v ) ) ;

suppose ( v1 = v & v2 = v ) ; :: thesis: e1 = e2

hence e1 = e2 by A1, A3, Def4; :: thesis: verum

end;

suppose A5: ( v1 = v & v2 <> v ) ; :: thesis: e1 = e2

per cases ( v2 in V or not v2 in V ) ;

suppose v2 in V ; :: thesis: e1 = e2

then consider e being object such that
( e in E & e Joins v2,v,G1 ) and
A6: for e3 being object st e3 Joins v2,v,G1 holds
e = e3 by A4;
( e1 = e & e2 = e ) by A6, A5, A3, GLIB_000:14;
hence e1 = e2 ; :: thesis: verum

end;

suppose not v2 in V ; :: thesis: e1 = e2

then not e1 Joins v2,v,G1 by A1, Def4;
hence e1 = e2 by A5, A3, GLIB_000:14; :: thesis: verum

end;

end;

end;

suppose A7: ( v1 <> v & v2 = v ) ; :: thesis: e1 = e2

per cases ( v1 in V or not v1 in V ) ;

suppose v1 in V ; :: thesis: e1 = e2

then consider e being object such that
( e in E & e Joins v1,v,G1 ) and
A8: for e3 being object st e3 Joins v1,v,G1 holds
e = e3 by A4;
( e1 Joins v1,v,G1 & e2 Joins v1,v,G1 ) by A7, A3;
then ( e1 = e & e2 = e ) by A8;
hence e1 = e2 ; :: thesis: verum

end;

suppose not v1 in V ; :: thesis: e1 = e2

hence e1 = e2 by A7, A3, A1, Def4; :: thesis: verum

end;

end;

end;

suppose ( v1 <> v & v2 <> v ) ; :: thesis: e1 = e2

then ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) by A1, A2, Def4;
hence e1 = e2 by GLIB_000:def 21; :: thesis: verum

end;

end;

end;

hence G1 is non-Dmulti by GLIB_000:def 21; :: thesis: verum

end;

suppose ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: G1 is non-Dmulti

then G1 == G by Def4;
hence G1 is non-Dmulti by GLIB_000:89; :: thesis: verum

end;

end;