now :: thesis: for x being object st x in _GraphSelectors holds
x in dom G
let x be object ; :: 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 Def10; :: thesis: verum
end;
then A1: _GraphSelectors c= dom G ;
set G2 = G | _GraphSelectors;
VertexSelector in _GraphSelectors by ENUMSET1:def 2;
then A2: the_Vertices_of (G | _GraphSelectors) = the_Vertices_of G by FUNCT_1:49;
EdgeSelector in _GraphSelectors by ENUMSET1:def 2;
then A3: the_Edges_of (G | _GraphSelectors) = the_Edges_of G by FUNCT_1:49;
TargetSelector in _GraphSelectors by ENUMSET1:def 2;
then A4: the_Target_of (G | _GraphSelectors) = the_Target_of G by FUNCT_1:49;
SourceSelector in _GraphSelectors by ENUMSET1:def 2;
then A5: the_Source_of (G | _GraphSelectors) = the_Source_of G by FUNCT_1:49;
dom (G | _GraphSelectors) = (dom G) /\ _GraphSelectors by RELAT_1:61
.= _GraphSelectors by A1, XBOOLE_1:28 ;
hence G | _GraphSelectors is [Graph-like] by A2, A3, A5, A4, Lm1; :: thesis: verum