let G2 be _Graph; for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
for e1, w being object st ( w <> v2 or e1 <> e ) holds
not e1 Joins v1,w,G1
let v1, e be object ; for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
for e1, w being object st ( w <> v2 or e1 <> e ) holds
not e1 Joins v1,w,G1
let v2 be Vertex of G2; for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
for e1, w being object st ( w <> v2 or e1 <> e ) holds
not e1 Joins v1,w,G1
let G1 be addAdjVertex of G2,v1,e,v2; ( not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 implies for e1, w being object st ( w <> v2 or e1 <> e ) holds
not e1 Joins v1,w,G1 )
assume A1:
( not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 )
; for e1, w being object st ( w <> v2 or e1 <> e ) holds
not e1 Joins v1,w,G1
let e1, w be object ; ( ( w <> v2 or e1 <> e ) implies not e1 Joins v1,w,G1 )
assume
( w <> v2 or e1 <> e )
; not e1 Joins v1,w,G1