set G9 = G | WGraphSelectors;
A1: G == G | WGraphSelectors by Lm4;
A2: the_Weight_of G = the_Weight_of (G | WGraphSelectors) by Lm4;
reconsider G9 = G | WGraphSelectors as [Weighted] Subgraph of G by A1, GLIB_000:87;
the_Weight_of G9 = (the_Weight_of G) | (the_Edges_of G9) by A2;
then reconsider G9 = G9 as WSubgraph of G by GLIB_003:def 10;
set Z = {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))};
set Y = union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))};
set X = Funcs (WGraphSelectors,(union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))}));
defpred S₁[ set ] means $1 is WSubgraph of G;
consider IT being Subset of (Funcs (WGraphSelectors,(union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))}))) such that
A3: for x being set holds
( x in IT iff ( x in Funcs (WGraphSelectors,(union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))})) & S₁[x] ) ) from SUBSET_1:sch 1();

A4: now :: thesis: for G2 being WSubgraph of G st dom G2 = WGraphSelectors holds
rng G2 c= union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))}

let G2 be WSubgraph of G; :: thesis: ( dom G2 = WGraphSelectors implies rng G2 c= union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} )
assume A5: dom G2 = WGraphSelectors ; :: thesis: rng G2 c= union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))}

now :: thesis: for y being object st y in rng G2 holds
y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))}

let y be object ; :: thesis: ( y in rng G2 implies y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} )
assume y in rng G2 ; :: thesis: y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))}
then consider x being object such that
A6: x in WGraphSelectors and
A7: G2 . x = y by A5, FUNCT_1:def 3;

now :: thesis: y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))}

per cases ( x = VertexSelector or x = EdgeSelector or x = SourceSelector or x = TargetSelector or x = WeightSelector ) by A6, ENUMSET1:def 3;

suppose A8: x = VertexSelector ; :: thesis: y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))}

A9: bool (the_Vertices_of G) in {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} by ENUMSET1:def 3;
y = the_Vertices_of G2 by A7, A8;
hence y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} by A9, TARSKI:def 4; :: thesis: verum

end;

suppose A10: x = EdgeSelector ; :: thesis: y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))}

A11: bool (the_Edges_of G) in {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} by ENUMSET1:def 3;
y = the_Edges_of G2 by A7, A10;
hence y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} by A11, TARSKI:def 4; :: thesis: verum

end;

suppose x = SourceSelector ; :: thesis: y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))}

then y = the_Source_of G2 by A7;
then y = (the_Source_of G) | (the_Edges_of G2) by GLIB_000:45;
then A12: G2 . x c= the_Source_of G by RELAT_1:59, A7;
bool (the_Source_of G) in {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} by ENUMSET1:def 3;
hence y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} by A12, TARSKI:def 4, A7; :: thesis: verum

end;

suppose x = TargetSelector ; :: thesis: y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))}

then y = the_Target_of G2 by A7;
then y = (the_Target_of G) | (the_Edges_of G2) by GLIB_000:45;
then A13: G2 . x c= the_Target_of G by RELAT_1:59, A7;
bool (the_Target_of G) in {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} by ENUMSET1:def 3;
hence y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} by A13, TARSKI:def 4, A7; :: thesis: verum

end;

suppose x = WeightSelector ; :: thesis: y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))}

then y = the_Weight_of G2 by A7;
then y = (the_Weight_of G) | (the_Edges_of G2) by GLIB_003:def 10;
then A14: G2 . x c= the_Weight_of G by RELAT_1:59, A7;
bool (the_Weight_of G) in {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} by ENUMSET1:def 3;
hence y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} by A14, TARSKI:def 4, A7; :: thesis: verum

end;

end;

end;

hence y in union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} ; :: thesis: verum

end;

hence rng G2 c= union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} ; :: thesis: verum

end;

A15: dom G9 = WGraphSelectors by Lm5;
then rng G9 c= union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} by A4;
then G9 in Funcs (WGraphSelectors,(union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))})) by A15, FUNCT_2:def 2;
then reconsider IT = IT as non empty set by A3;
take IT ; :: thesis: for x being set holds
( x in IT iff ex G2 being WSubgraph of G st
( x = G2 & dom G2 = WGraphSelectors ) )
let x be set ; :: thesis: ( x in IT iff ex G2 being WSubgraph of G st
( x = G2 & dom G2 = WGraphSelectors ) )

hereby :: thesis: ( ex G2 being WSubgraph of G st
( x = G2 & dom G2 = WGraphSelectors ) implies x in IT )

assume A16: x in IT ; :: thesis: ex x9 being WSubgraph of G st
( x9 = x & dom x9 = WGraphSelectors )
then reconsider x9 = x as WSubgraph of G by A3;
take x9 = x9; :: thesis: ( x9 = x & dom x9 = WGraphSelectors )
thus x9 = x ; :: thesis: dom x9 = WGraphSelectors
ex f being Function st
( f = x & dom f = WGraphSelectors & rng f c= union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} ) by A16, FUNCT_2:def 2;
hence dom x9 = WGraphSelectors ; :: thesis: verum

end;

given G2 being WSubgraph of G such that A17: G2 = x and
A18: dom G2 = WGraphSelectors ; :: thesis: x in IT
rng G2 c= union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))} by A4, A18;
then x in Funcs (WGraphSelectors,(union {(bool (the_Vertices_of G)),(bool (the_Edges_of G)),(bool (the_Source_of G)),(bool (the_Target_of G)),(bool (the_Weight_of G))})) by A17, A18, FUNCT_2:def 2;
hence x in IT by A3, A17; :: thesis: verum