let IT1, IT2 be non empty set ; :: thesis: ( ( for x being set holds
( x in IT1 iff ex G2 being WSubgraph of G st
( x = G2 & dom G2 = WGraphSelectors ) ) ) & ( for x being set holds
( x in IT2 iff ex G2 being WSubgraph of G st
( x = G2 & dom G2 = WGraphSelectors ) ) ) implies IT1 = IT2 )
assume that
A19: for x being set holds
( x in IT1 iff ex G2 being WSubgraph of G st
( x = G2 & dom G2 = WGraphSelectors ) ) and
A20: for x being set holds
( x in IT2 iff ex G2 being WSubgraph of G st
( x = G2 & dom G2 = WGraphSelectors ) ) ; :: thesis: IT1 = IT2

now :: thesis: for x being object holds
( x in IT1 iff x in IT2 )

let x be object ; :: thesis: ( x in IT1 iff x in IT2 )
( x in IT1 iff ex G2 being WSubgraph of G st
( x = G2 & dom G2 = WGraphSelectors ) ) by A19;
hence ( x in IT1 iff x in IT2 ) by A20; :: thesis: verum

end;

hence IT1 = IT2 by TARSKI:2; :: thesis: verum