let X1, X2 be set ; :: thesis: ( ( for E being object holds
( E in X1 iff ex G being _Graph st
( G in S & E = the_Edges_of G ) ) ) & ( for E being object holds
( E in X2 iff ex G being _Graph st
( G in S & E = the_Edges_of G ) ) ) implies X1 = X2 )
assume that
A7: for E being object holds
( E in X1 iff ex G being _Graph st
( G in S & E = the_Edges_of G ) ) and
A8: for E being object holds
( E in X2 iff ex G being _Graph st
( G in S & E = the_Edges_of G ) ) ; :: thesis: X1 = X2

now :: thesis: for E being object holds
( ( E in X1 implies E in X2 ) & ( E in X2 implies E in X1 ) )

let E be object ; :: thesis: ( ( E in X1 implies E in X2 ) & ( E in X2 implies E in X1 ) )

hereby :: thesis: ( E in X2 implies E in X1 )

assume E in X1 ; :: thesis: E in X2
then ex G being _Graph st
( G in S & E = the_Edges_of G ) by A7;
hence E in X2 by A8; :: thesis: verum

end;

assume E in X2 ; :: thesis: E in X1
then ex G being _Graph st
( G in S & E = the_Edges_of G ) by A8;
hence E in X1 by A7; :: thesis: verum

end;

hence X1 = X2 by TARSKI:2; :: thesis: verum