let G1 be addAdjVertexAll of G,v,V; G1 is non-multi
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 )
;
G1 is non-multi
for
e1,
e2,
v1,
v2 being
object st
e1 Joins v1,
v2,
G1 &
e2 Joins v1,
v2,
G1 holds
e1 = e2
proof
let e1,
e2,
v1,
v2 be
object ;
( e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 implies e1 = e2 )
assume A2:
(
e1 Joins v1,
v2,
G1 &
e2 Joins v1,
v2,
G1 )
;
e1 = e2
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 A3:
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 ) )
;
end;
end; hence
G1 is
non-multi
by GLIB_000:def 20;
verum end; end;