let G be WGraph; :: thesis: WGraphSelectors c= dom G

now

let x be set ; :: thesis: ( x in WGraphSelectors implies x in dom G )
assume x in WGraphSelectors ; :: thesis: x in dom G
then ( x = VertexSelector or x = EdgeSelector or x = SourceSelector or x = TargetSelector or x = WeightSelector ) by ENUMSET1:def 3;
hence x in dom G by GLIB_000:def 11, GLIB_003:def 4; :: thesis: verum

end;

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