let G be WGraph; :: thesis: WGraphSelectors c= dom G
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in WGraphSelectors or 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 10, GLIB_003:def 4; :: thesis: verum