let G, G2 be _Graph; for v being object
for V being set
for G1 being addAdjVertexToAll of G,v,V st G1 == G2 holds
G2 is addAdjVertexToAll of G,v,V
let v be object ; for V being set
for G1 being addAdjVertexToAll of G,v,V st G1 == G2 holds
G2 is addAdjVertexToAll of G,v,V
let V be set ; for G1 being addAdjVertexToAll of G,v,V st G1 == G2 holds
G2 is addAdjVertexToAll of G,v,V
let G1 be addAdjVertexToAll of G,v,V; ( G1 == G2 implies G2 is addAdjVertexToAll of G,v,V )
assume A1:
G1 == G2
; G2 is addAdjVertexToAll of G,v,V