let G2 be _Graph; for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 <> v & v2 <> v & e Joins v1,v2,G1 holds
e Joins v1,v2,G2
let v be object ; for V being set
for G1 being addAdjVertexAll of G2,v,V
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 <> v & v2 <> v & e Joins v1,v2,G1 holds
e Joins v1,v2,G2
let V be set ; for G1 being addAdjVertexAll of G2,v,V
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 <> v & v2 <> v & e Joins v1,v2,G1 holds
e Joins v1,v2,G2
let G1 be addAdjVertexAll of G2,v,V; for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 <> v & v2 <> v & e Joins v1,v2,G1 holds
e Joins v1,v2,G2
let v1, e, v2 be object ; ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 <> v & v2 <> v & e Joins v1,v2,G1 implies e Joins v1,v2,G2 )
assume that
A1:
( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 )
and
A2:
( v1 <> v & v2 <> v )
and
A3:
e Joins v1,v2,G1
; e Joins v1,v2,G2