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