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