set GS = _GraphSelectors ;
let G be _Graph; for X being set holds
( G .set (WeightSelector,X) == G & G .set (ELabelSelector,X) == G & G .set (VLabelSelector,X) == G )
let X be set ; ( 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; ( 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; 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; verum