set GS = _GraphSelectors ;
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 G2 = G .set WeightSelector ,X;
A1: not WeightSelector in _GraphSelectors by ENUMSET1:def 2;
then A2: ( 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;
( the_Vertices_of (G .set WeightSelector ,X) = the_Vertices_of G & the_Edges_of (G .set WeightSelector ,X) = the_Edges_of G ) by A1, GLIB_000:13;
hence G .set WeightSelector ,X == G by A2, GLIB_000:def 36; :: thesis: ( G .set ELabelSelector ,X == G & G .set VLabelSelector ,X == G )
set G2 = G .set ELabelSelector ,X;
A3: not ELabelSelector in _GraphSelectors by ENUMSET1:def 2;
then A4: ( 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;
( the_Vertices_of (G .set ELabelSelector ,X) = the_Vertices_of G & the_Edges_of (G .set ELabelSelector ,X) = the_Edges_of G ) by A3, GLIB_000:13;
hence G .set ELabelSelector ,X == G by A4, GLIB_000:def 36; :: thesis: G .set VLabelSelector ,X == G
set G2 = G .set VLabelSelector ,X;
A5: not VLabelSelector in _GraphSelectors by ENUMSET1:def 2;
then A6: ( 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;
( the_Vertices_of (G .set VLabelSelector ,X) = the_Vertices_of G & the_Edges_of (G .set VLabelSelector ,X) = the_Edges_of G ) by A5, GLIB_000:13;
hence G .set VLabelSelector ,X == G by A6, GLIB_000:def 36; :: thesis: verum