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; 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; verum