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:

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

now :: thesis:

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

now :: thesis:

per cases by A3, ENUMSET1:def 3;

suppose A5: x = VertexSelector ; :: thesis:

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:

end;

suppose A7: x = EdgeSelector ; :: thesis:

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:

end;

suppose x = SourceSelector ; :: thesis:

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:

end;

suppose x = TargetSelector ; :: thesis:

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:

end;

suppose x = WeightSelector ; :: thesis:

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:

end;

end;

end;

hence y in Y ; :: thesis:

end;

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

end;

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