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:10;
( 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:10;
hence G .set (WeightSelector,X) == G by A2; :: 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:10;
( 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:10;
hence G .set (ELabelSelector,X) == G by A4; :: 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:10;
( 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:10;
hence G .set (VLabelSelector,X) == G by A6; :: thesis: verum