set G2 = G .strict _GraphSelectors ;

now

let x be set ; :: thesis: ( x in _GraphSelectors implies x in dom G )
assume x in _GraphSelectors ; :: thesis: x in dom G
then ( x = VertexSelector or x = EdgeSelector or x = SourceSelector or x = TargetSelector ) by ENUMSET1:def 2;
hence x in dom G by Def11; :: thesis: verum

end;

then A1: _GraphSelectors c= dom G by TARSKI:def 3;
A2: dom (G .strict _GraphSelectors ) = (dom G) /\ _GraphSelectors by RELAT_1:90
.= _GraphSelectors by A1, XBOOLE_1:28 ;
A3: ( VertexSelector in _GraphSelectors & EdgeSelector in _GraphSelectors & SourceSelector in _GraphSelectors & TargetSelector in _GraphSelectors ) by ENUMSET1:def 2;
then A4: the_Vertices_of (G .strict _GraphSelectors ) = the_Vertices_of G by FUNCT_1:72;
A5: the_Edges_of (G .strict _GraphSelectors ) = the_Edges_of G by A3, FUNCT_1:72;
A6: the_Source_of (G .strict _GraphSelectors ) = the_Source_of G by A3, FUNCT_1:72;
the_Target_of (G .strict _GraphSelectors ) = the_Target_of G by A3, FUNCT_1:72;
hence G .strict _GraphSelectors is [Graph-like] by A2, A4, A5, A6, Lm1; :: thesis: verum