let G be VGraph; :: thesis: for v, x being set st v in the_Vertices_of G holds
G .labeledV() c= (G .labelVertex (v,x)) .labeledV()
let e, x be set ; :: thesis: ( e in the_Vertices_of G implies G .labeledV() c= (G .labelVertex (e,x)) .labeledV() )
assume e in the_Vertices_of G ; :: thesis: G .labeledV() c= (G .labelVertex (e,x)) .labeledV()
then (G .labelVertex (e,x)) .labeledV() = (G .labeledV()) \/ {e} by Th52;
hence G .labeledV() c= (G .labelVertex (e,x)) .labeledV() by XBOOLE_1:7; :: thesis: verum