let G be VGraph; :: thesis: for v1, v2, x being set st not v2 in G .labeledV() & v2 in (G .labelVertex (v1,x)) .labeledV() holds
( v1 = v2 & v1 in the_Vertices_of G )
let e1, e2, val be set ; :: thesis: ( not e2 in G .labeledV() & e2 in (G .labelVertex (e1,val)) .labeledV() implies ( e1 = e2 & e1 in the_Vertices_of G ) )
set Gn = G .labelVertex (e1,val);
assume that
A1: not e2 in G .labeledV() and
A2: e2 in (G .labelVertex (e1,val)) .labeledV() ; :: thesis: ( e1 = e2 & e1 in the_Vertices_of G )
e1 in the_Vertices_of G by A1, A2, Def22;
then the_VLabel_of (G .labelVertex (e1,val)) = (the_VLabel_of G) +* (e1 .--> val) by Th38;
then ( e2 in dom (the_VLabel_of G) or e2 in dom (e1 .--> val) ) by A2, FUNCT_4:12;
then e2 in {e1} by A1;
hence e1 = e2 by TARSKI:def 1; :: thesis: e1 in the_Vertices_of G
thus e1 in the_Vertices_of G by A1, A2, Def22; :: thesis: verum