let x be Element of X; :: thesis: x is WSubgraph of G
consider G2 being WSubgraph of G such that
A1: ( G2 = x & dom G2 = WGraphSelectors ) by Def10;
thus x is WSubgraph of G by A1; :: thesis: verum