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:72;
A4: SourceSelector in WGraphSelectors by ENUMSET1:def 3;
then A5: the_Source_of (G | WGraphSelectors) = the_Source_of G by FUNCT_1:72;
A6: EdgeSelector in WGraphSelectors by ENUMSET1:def 3;
then A7: the_Edges_of (G | WGraphSelectors) = the_Edges_of G by FUNCT_1:72;
A8: dom (G | WGraphSelectors) = (dom G) /\ WGraphSelectors by RELAT_1:90
.= WGraphSelectors by Lm3, XBOOLE_1:28 ;
then for x being set 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) by TARSKI:def 3;
the_Vertices_of (G | WGraphSelectors) = the_Vertices_of G by A1, FUNCT_1:72;
hence G | WGraphSelectors is [Graph-like] by A7, A5, A3, A9, GLIB_000:7; :: thesis: G | WGraphSelectors is [Weighted]
A10: WeightSelector in WGraphSelectors by ENUMSET1:def 3;
then (G | WGraphSelectors) . WeightSelector = G . WeightSelector by FUNCT_1:72;
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, GLIB_003:def 4; :: thesis: verum