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

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