let G be WGraph; :: thesis: ( G == G | WGraphSelectors & the_Weight_of G = the_Weight_of (G | WGraphSelectors) )
set G2 = G | WGraphSelectors;
EdgeSelector in WGraphSelectors by ENUMSET1:def 3;
then A1: the_Edges_of (G | WGraphSelectors) = the_Edges_of G by FUNCT_1:49;
SourceSelector in WGraphSelectors by ENUMSET1:def 3;
then A2: the_Source_of (G | WGraphSelectors) = the_Source_of G by FUNCT_1:49;
TargetSelector in WGraphSelectors by ENUMSET1:def 3;
then A3: the_Target_of (G | WGraphSelectors) = the_Target_of G by FUNCT_1:49;
VertexSelector in WGraphSelectors by ENUMSET1:def 3;
then the_Vertices_of (G | WGraphSelectors) = the_Vertices_of G by FUNCT_1:49;
hence G == G | WGraphSelectors by A1, A2, A3; :: thesis: the_Weight_of G = the_Weight_of (G | WGraphSelectors)
WeightSelector in WGraphSelectors by ENUMSET1:def 3;
hence the_Weight_of G = the_Weight_of (G | WGraphSelectors) by FUNCT_1:49; :: thesis: verum