set G2 = G .strict WGraphSelectors ;
A1: VertexSelector in WGraphSelectors by ENUMSET1:def 3;
A2: TargetSelector in WGraphSelectors by ENUMSET1:def 3;
then A3: the_Target_of (G .strict WGraphSelectors ) = the_Target_of G by FUNCT_1:72;
A4: SourceSelector in WGraphSelectors by ENUMSET1:def 3;
then A5: the_Source_of (G .strict WGraphSelectors ) = the_Source_of G by FUNCT_1:72;
A6: EdgeSelector in WGraphSelectors by ENUMSET1:def 3;
then A7: the_Edges_of (G .strict WGraphSelectors ) = the_Edges_of G by FUNCT_1:72;
A8: dom (G .strict 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 .strict WGraphSelectors ) by A1, A6, A4, A2, ENUMSET1:def 2;
then A9: _GraphSelectors c= dom (G .strict WGraphSelectors ) by TARSKI:def 3;
the_Vertices_of (G .strict WGraphSelectors ) = the_Vertices_of G by A1, FUNCT_1:72;
hence G .strict WGraphSelectors is [Graph-like] by A7, A5, A3, A9, GLIB_000:7; :: thesis: G .strict WGraphSelectors is [Weighted]
A10: WeightSelector in WGraphSelectors by ENUMSET1:def 3;
then (G .strict WGraphSelectors ) . WeightSelector = G . WeightSelector by FUNCT_1:72;
then (G .strict WGraphSelectors ) . WeightSelector is ManySortedSet of the_Edges_of (G .strict WGraphSelectors ) by A7, GLIB_003:def 4;
hence G .strict WGraphSelectors is [Weighted] by A8, A10, GLIB_003:def 4; :: thesis: verum