let G2 be WSubgraph of G; :: thesis: G2 is real-weighted
set W2 = (the_Weight_of G) | (the_Edges_of G2);
the_Weight_of G2 = (the_Weight_of G) | (the_Edges_of G2) by Def10;
hence G2 is real-weighted ; :: thesis: verum