let G2 be VSubgraph of G; :: thesis: G2 is real-vlabeled
the_VLabel_of G2 = (the_VLabel_of G) | (the_Vertices_of G2) by Def12;
hence G2 is real-vlabeled ; :: thesis: verum