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))};
for x being set st x 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))} holds
x is finite by ENUMSET1:def 3;
then reconsider 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))} as finite set by FINSET_1:7;
set X = Funcs (WGraphSelectors,Y);

now :: thesis: for x being object st x in G .allWSubgraphs() holds
x in Funcs (WGraphSelectors,Y)

let x be object ; :: thesis: ( x in G .allWSubgraphs() implies x in Funcs (WGraphSelectors,Y) )
assume x in G .allWSubgraphs() ; :: thesis: x in Funcs (WGraphSelectors,Y)
then consider G2 being WSubgraph of G such that
A1: x = G2 and
A2: dom G2 = WGraphSelectors by Def5;

now :: thesis: for y being object st y in rng G2 holds
y in Y

let y be object ; :: thesis: ( y in rng G2 implies y in Y )
assume y in rng G2 ; :: thesis: y in Y
then consider x being object such that
A3: x in WGraphSelectors and
A4: G2 . x = y by A2, FUNCT_1:def 3;

now :: thesis: y in Y

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

suppose A5: x = VertexSelector ; :: thesis: y in Y

A6: 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 A4, A5;
hence y in Y by A6, TARSKI:def 4; :: thesis: verum

end;

suppose A7: x = EdgeSelector ; :: thesis: y in Y

A8: 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 A4, A7;
hence y in Y by A8, TARSKI:def 4; :: thesis: verum

end;

suppose x = SourceSelector ; :: thesis: y in Y

then y = the_Source_of G2 by A4;
then y = (the_Source_of G) | (the_Edges_of G2) by GLIB_000:45;
then A9: G2 . x c= the_Source_of G by RELAT_1:59, A4;
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 Y by A9, TARSKI:def 4, A4; :: thesis: verum

end;

suppose x = TargetSelector ; :: thesis: y in Y

then y = the_Target_of G2 by A4;
then y = (the_Target_of G) | (the_Edges_of G2) by GLIB_000:45;
then A10: G2 . x c= the_Target_of G by RELAT_1:59, A4;
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 Y by A10, TARSKI:def 4, A4; :: thesis: verum

end;

suppose x = WeightSelector ; :: thesis: y in Y

then y = the_Weight_of G2 by A4;
then y = (the_Weight_of G) | (the_Edges_of G2) by GLIB_003:def 10;
then A11: G2 . x c= the_Weight_of G by RELAT_1:59, A4;
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 Y by A11, TARSKI:def 4, A4; :: thesis: verum

end;

end;

end;

hence y in Y ; :: thesis: verum

end;

then rng G2 c= Y ;
hence x in Funcs (WGraphSelectors,Y) by A1, A2, FUNCT_2:def 2; :: thesis: verum

end;

then G .allWSubgraphs() c= Funcs (WGraphSelectors,Y) ;
hence G .allWSubgraphs() is finite ; :: thesis: verum