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:25;
set X = Funcs WGraphSelectors ,Y;

now

let x be set ; :: 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
A2: ( x = G2 & dom G2 = WGraphSelectors ) by Def10;

now

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

now

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

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

then A4: y = the_Vertices_of G2 by A3;
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;
hence y in Y by A4, TARSKI:def 4; :: thesis: verum

end;

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

then A5: y = the_Edges_of G2 by A3;
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;
hence y in Y by A5, TARSKI:def 4; :: thesis: verum

end;

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

then y = the_Source_of G2 by A3;
then y = (the_Source_of G) | (the_Edges_of G2) by GLIB_000:48;
then A6: y c= the_Source_of G by RELAT_1:88;
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 A6, TARSKI:def 4; :: thesis: verum

end;

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

then y = the_Target_of G2 by A3;
then y = (the_Target_of G) | (the_Edges_of G2) by GLIB_000:48;
then A7: y c= the_Target_of G by RELAT_1:88;
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 A7, TARSKI:def 4; :: thesis: verum

end;

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

then y = the_Weight_of G2 by A3;
then y = (the_Weight_of G) | (the_Edges_of G2) by GLIB_003:def 10;
then A8: y c= the_Weight_of G by RELAT_1:88;
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 A8, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence y in Y ; :: thesis: verum

end;

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

end;

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