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 Th45;
then ( e2 in dom (the_VLabel_of G) or e2 in dom (e1 .--> val) ) by A2, FUNCT_4:13;
then e2 in {e1} by A1, FUNCOP_1:19;
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