let G be _Graph; :: thesis: _GraphSelectors c= dom G

now :: thesis: for x being set st x in _GraphSelectors holds
x in dom G

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 Def10; :: thesis: verum

end;

hence _GraphSelectors c= dom G by TARSKI:def 3; :: thesis: verum