for G1, G2 being _Graph
for F being semi-continuous PGraphMapping of G1,G2
for v1, v2 being object st v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 & ex e, w being object st
( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v1,(F _V) . w,G2 ) holds
v1 = v2