let G be _Graph; :: thesis: for X being set holds
( G .set WeightSelector ,X == G & G .set ELabelSelector ,X == G & G .set VLabelSelector ,X == G )
let X be set ; :: thesis: ( G .set WeightSelector ,X == G & G .set ELabelSelector ,X == G & G .set VLabelSelector ,X == G )
set GS = _GraphSelectors ;
set G2 = G .set WeightSelector ,X;
not WeightSelector in _GraphSelectors by ENUMSET1:def 2;
then ( the_Vertices_of (G .set WeightSelector ,X) = the_Vertices_of G & the_Edges_of (G .set WeightSelector ,X) = the_Edges_of G & the_Source_of (G .set WeightSelector ,X) = the_Source_of G & the_Target_of (G .set WeightSelector ,X) = the_Target_of G ) by GLIB_000:13;
hence G .set WeightSelector ,X == G by GLIB_000:def 36; :: thesis: ( G .set ELabelSelector ,X == G & G .set VLabelSelector ,X == G )
set G2 = G .set ELabelSelector ,X;
not ELabelSelector in _GraphSelectors by ENUMSET1:def 2;
then ( the_Vertices_of (G .set ELabelSelector ,X) = the_Vertices_of G & the_Edges_of (G .set ELabelSelector ,X) = the_Edges_of G & the_Source_of (G .set ELabelSelector ,X) = the_Source_of G & the_Target_of (G .set ELabelSelector ,X) = the_Target_of G ) by GLIB_000:13;
hence G .set ELabelSelector ,X == G by GLIB_000:def 36; :: thesis: G .set VLabelSelector ,X == G
set G2 = G .set VLabelSelector ,X;
not VLabelSelector in _GraphSelectors by ENUMSET1:def 2;
then ( the_Vertices_of (G .set VLabelSelector ,X) = the_Vertices_of G & the_Edges_of (G .set VLabelSelector ,X) = the_Edges_of G & the_Source_of (G .set VLabelSelector ,X) = the_Source_of G & the_Target_of (G .set VLabelSelector ,X) = the_Target_of G ) by GLIB_000:13;
hence G .set VLabelSelector ,X == G by GLIB_000:def 36; :: thesis: verum