let G1 be addAdjVertexAll of G,v,V; G1 is loopless
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 loopless
for
e being
object holds
( not
e in the_Edges_of G1 or not
(the_Source_of G1) . e = (the_Target_of G1) . e )
proof
given e being
object such that A2:
e in the_Edges_of G1
and A3:
(the_Source_of G1) . e = (the_Target_of G1) . e
;
contradiction
per cases
( (the_Source_of G1) . e = v or (the_Source_of G1) . e <> v )
;
suppose A4:
(the_Source_of G1) . e <> v
;
contradiction
e DJoins (the_Source_of G1) . e,
(the_Target_of G1) . e,
G1
by A2, GLIB_000:def 14;
then
e DJoins (the_Source_of G1) . e,
(the_Source_of G1) . e,
G
by A3, A1, A4, Def4;
then
e Joins (the_Source_of G1) . e,
(the_Source_of G1) . e,
G
by GLIB_000:16;
hence
contradiction
by GLIB_000:18;
verum end; end;
end; hence
G1 is
loopless
by GLIB_000:def 18;
verum end; end;