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