let G2 be _Graph; for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
not G1 is edgeless
let v1 be Vertex of G2; for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
not G1 is edgeless
let e, v2 be object ; for G1 being addAdjVertex of G2,v1,e,v2 st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
not G1 is edgeless
let G1 be addAdjVertex of G2,v1,e,v2; ( not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 implies not G1 is edgeless )
assume
( not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 )
; not G1 is edgeless
then
the_Edges_of G1 = (the_Edges_of G2) \/ {e}
by GLIB_006:def 13;
hence
not G1 is edgeless
; verum