let x be Element of X; :: thesis: x is WSubgraph of G
ex G2 being WSubgraph of G st
( G2 = x & dom G2 = WGraphSelectors ) by Def5;
hence x is WSubgraph of G ; :: thesis: verum