let G be _Graph; :: thesis: G == G | _GraphSelectors
A1: ( VertexSelector in _GraphSelectors & EdgeSelector in _GraphSelectors & SourceSelector in _GraphSelectors & TargetSelector in _GraphSelectors ) by ENUMSET1:def 2;
A2: the_Vertices_of G = the_Vertices_of (G | _GraphSelectors) by A1, FUNCT_1:49;
A3: the_Edges_of G = the_Edges_of (G | _GraphSelectors) by A1, FUNCT_1:49;
A4: the_Source_of G = the_Source_of (G | _GraphSelectors) by A1, FUNCT_1:49;
the_Target_of G = the_Target_of (G | _GraphSelectors) by A1, FUNCT_1:49;
hence G == G | _GraphSelectors by A2, A3, A4; :: thesis: verum