let G1 be addAdjVertex of G,v1,e,v2; G1 is non-multi
per cases
( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ) )
;
suppose A1:
(
v1 in the_Vertices_of G & not
v2 in the_Vertices_of G & not
e in the_Edges_of G )
;
G1 is non-multi consider G3 being
addVertex of
G,
v2 such that A2:
G1 is
addEdge of
G3,
v1,
e,
v2
by A1, Th129;
reconsider w1 =
v1 as
Vertex of
G3 by A1, Th72;
reconsider w2 =
v2 as
Vertex of
G3 by Th98;
for
e1 being
object holds not
e1 Joins w1,
w2,
G3
then A5:
not
w1,
w2 are_adjacent
by CHORD:def 3;
thus
G1 is
non-multi
by A2, A5, Th120;
verum end; suppose A6:
( not
v1 in the_Vertices_of G &
v2 in the_Vertices_of G & not
e in the_Edges_of G )
;
G1 is non-multi consider G3 being
addVertex of
G,
v1 such that A7:
G1 is
addEdge of
G3,
v1,
e,
v2
by A6, Th130;
reconsider w2 =
v2 as
Vertex of
G3 by A6, Th72;
reconsider w1 =
v1 as
Vertex of
G3 by Th98;
for
e1 being
object holds not
e1 Joins w1,
w2,
G3
hence
G1 is
non-multi
by A7, Th120, CHORD:def 3;
verum end; end;