set G' = G .strict WGraphSelectors ;
A1: G == G .strict WGraphSelectors by Lm4;
A2: the_Weight_of G = the_Weight_of (G .strict WGraphSelectors ) by Lm4;
reconsider G' = G .strict WGraphSelectors as [Weighted] Subgraph of G by A1, 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 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 ;
consider IT being Subset of 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

let G2 be WSubgraph of ; :: 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 and
A7: 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 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:48;
then A12: 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 A12, 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 A7;
then y = (the_Target_of G) | (the_Edges_of G2) by GLIB_000:48;
then A13: 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 A13, 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 A7;
then y = (the_Weight_of G) | (the_Edges_of G2) by GLIB_003:def 10;
then A14: 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 A14, 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;

A15: dom G' = WGraphSelectors by Lm5;
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 A4;
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 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 st
( x = G2 & dom G2 = WGraphSelectors ) )
let x be set ; :: thesis: ( x in IT iff ex G2 being WSubgraph of st
( x = G2 & dom G2 = WGraphSelectors ) )

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

assume A16: x in IT ; :: thesis: ex x' being WSubgraph of st
( x' = x & dom x' = WGraphSelectors )
then reconsider x' = x as WSubgraph of by A3;
take x' = x'; :: thesis: ( x' = x & dom x' = WGraphSelectors )
thus x' = x ; :: thesis: dom x' = 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 x' = WGraphSelectors ; :: thesis: verum

end;

given G2 being WSubgraph of 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