let G be WGraph; :: thesis: dom (G | WGraphSelectors ) = WGraphSelectors
WGraphSelectors c= dom G by Lm3;
hence dom (G | WGraphSelectors ) = WGraphSelectors by RELAT_1:91; :: thesis: verum