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