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