let G1, G2 be _Graph; :: thesis: 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
let F be semi-continuous PGraphMapping of G1,G2; :: thesis: 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
let v1, v2 be object ; :: thesis: ( 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 ) implies v1 = v2 )
assume that
A1: ( v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 ) and
A2: 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 ) ; :: thesis: v1 = v2
consider e, w being object such that
A3: ( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v1,(F _V) . w,G2 ) by A2;
A4: e Joins v1,w,G1 by A1, A3, Def15;
e Joins v2,w,G1 by A1, A3, Def15;

per cases then ( ( v1 = v2 & w = w ) or ( v1 = w & w = v2 ) ) by A4, GLIB_000:15;

suppose ( v1 = v2 & w = w ) ; :: thesis: v1 = v2

hence v1 = v2 ; :: thesis: verum

end;

suppose ( v1 = w & w = v2 ) ; :: thesis: v1 = v2

hence v1 = v2 ; :: thesis: verum

end;

end;