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
A1: 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();
set G' = G .strict WGraphSelectors ;
A2: ( G == G .strict WGraphSelectors & the_Weight_of G = the_Weight_of (G .strict WGraphSelectors ) ) by Lm2;
then reconsider G' = G .strict WGraphSelectors as [Weighted] Subgraph of G by GLIB_000:90;
dom (the_Weight_of G) = the_Edges_of G' by A2, PARTFUN1:def 4;
then the_Weight_of G' = (the_Weight_of G) | (the_Edges_of G') by A2, RELAT_1:98;
then reconsider G' = G' as WSubgraph of G by GLIB_003:def 10;
A3: dom G' = WGraphSelectors by Lm3;

A4: now

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

let y be set ; :: 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 set such that
A6: ( x in WGraphSelectors & G2 . x = y ) by A5, FUNCT_1:def 5;

now

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

suppose 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))}

then A7: y = the_Vertices_of G2 by 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;
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 A7, TARSKI:def 4; :: thesis: verum

end;

suppose 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))}

then A8: y = the_Edges_of G2 by A6;
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 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 A8, 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 A6;
then y = (the_Source_of G) | (the_Edges_of G2) by GLIB_000:48;
then A9: 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 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 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 A6;
then y = (the_Target_of G) | (the_Edges_of G2) by GLIB_000:48;
then A10: 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 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 A10, TARSKI:def 4; :: 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 A6;
then y = (the_Weight_of G) | (the_Edges_of G2) by GLIB_003:def 10;
then A11: 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 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;

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))} by TARSKI:def 3; :: thesis: verum

end;

then rng G' 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 A3;
then G' 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 A3, FUNCT_2:def 2;
then reconsider IT = IT as non empty set by A1;
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 A12: x in IT ; :: thesis: ex x' being WSubgraph of G st
( x' = x & dom x' = WGraphSelectors )
then reconsider x' = x as WSubgraph of G by A1;
take x' = x'; :: thesis: ( x' = x & dom x' = WGraphSelectors )
thus x' = x ; :: thesis: dom x' = WGraphSelectors
consider f being Function such that
A13: ( 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 A12, FUNCT_2:def 2;
thus dom x' = WGraphSelectors by A13; :: thesis: verum

end;

given G2 being WSubgraph of G such that A14: ( G2 = x & 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, A14;
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 A14, FUNCT_2:def 2;
hence x in IT by A1, A14; :: thesis: verum