set G2 = G | WGraphSelectors;
A1: VertexSelector in WGraphSelectors by ENUMSET1:def 3;
A2: TargetSelector in WGraphSelectors by ENUMSET1:def 3;
then A3: the_Target_of (G | WGraphSelectors) = the_Target_of G by FUNCT_1:49;
A4: SourceSelector in WGraphSelectors by ENUMSET1:def 3;
then A5: the_Source_of (G | WGraphSelectors) = the_Source_of G by FUNCT_1:49;
A6: EdgeSelector in WGraphSelectors by ENUMSET1:def 3;
then A7: the_Edges_of (G | WGraphSelectors) = the_Edges_of G by FUNCT_1:49;
A8: dom (G | WGraphSelectors) = (dom G) /\ WGraphSelectors by RELAT_1:61
.= WGraphSelectors by Lm3, XBOOLE_1:28 ;
then for x being object st x in _GraphSelectors holds
x in dom (G | WGraphSelectors) by A1, A6, A4, A2, ENUMSET1:def 2;
then A9: _GraphSelectors c= dom (G | WGraphSelectors) ;
the_Vertices_of (G | WGraphSelectors) = the_Vertices_of G by A1, FUNCT_1:49;
hence G | WGraphSelectors is [Graph-like] by A7, A5, A3, A9, GLIB_000:5; :: thesis: G | WGraphSelectors is [Weighted]
A10: WeightSelector in WGraphSelectors by ENUMSET1:def 3;
then (G | WGraphSelectors) . WeightSelector = G . WeightSelector by FUNCT_1:49;
then (G | WGraphSelectors) . WeightSelector is ManySortedSet of the_Edges_of (G | WGraphSelectors) by A7, GLIB_003:def 4;
hence G | WGraphSelectors is [Weighted] by A8, A10; :: thesis: verum