hereby :: thesis: ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ex b₁ being Supergraph of G st b₁ == G )

assume A1: ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: ex G1 being Supergraph of G st
( the_Vertices_of G1 = (the_Vertices_of G) \/ {v} & ( for e being object holds
( not e Joins v,v,G1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G & the_Edges_of G1 = (the_Edges_of G) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) ) )
reconsider G1 = the addAdjVertexToAll of G,v,V as Supergraph of G ;
take G1 = G1; :: thesis: ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v} & ( for e being object holds
( not e Joins v,v,G1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G & the_Edges_of G1 = (the_Edges_of G) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) ) )
thus the_Vertices_of G1 = (the_Vertices_of G) \/ {v} by A1, Def2; :: thesis: ( ( for e being object holds
( not e Joins v,v,G1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G & the_Edges_of G1 = (the_Edges_of G) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) ) )
thus ( ( for e being object holds
( not e Joins v,v,G1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G & the_Edges_of G1 = (the_Edges_of G) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) ) ) by A1, Lm9; :: thesis: verum

end;

assume ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: ex b₁ being Supergraph of G st b₁ == G
reconsider G1 = G as Supergraph of G by GLIB_006:61;
take G1 ; :: thesis: G1 == G
thus G1 == G ; :: thesis: verum