dom W = the_Edges_of G by FUNCT_2:def 1;
then reconsider W' = W as ManySortedSet of the_Edges_of G by PBOOLE:def 3;
G .set WeightSelector ,W' is [Weighted] ;
hence G .set WeightSelector ,W is [Weighted] ; :: thesis: verum