let G be _Graph; for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for e, v, w being object st e Joins v,w,G holds
e Joins V . v,V . w, replaceVertices V
let V be non empty one-to-one ManySortedSet of the_Vertices_of G; for e, v, w being object st e Joins v,w,G holds
e Joins V . v,V . w, replaceVertices V
let e, v, w be object ; ( e Joins v,w,G implies e Joins V . v,V . w, replaceVertices V )
assume
e Joins v,w,G
; e Joins V . v,V . w, replaceVertices V