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