let X1, X2 be set ; :: thesis: ( ( for t being object holds
( t in X1 iff ex G being _Graph st
( G in S & t = the_Target_of G ) ) ) & ( for t being object holds
( t in X2 iff ex G being _Graph st
( G in S & t = the_Target_of G ) ) ) implies X1 = X2 )
assume that
A15: for t being object holds
( t in X1 iff ex G being _Graph st
( G in S & t = the_Target_of G ) ) and
A16: for t being object holds
( t in X2 iff ex G being _Graph st
( G in S & t = the_Target_of G ) ) ; :: thesis: X1 = X2

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

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

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

assume t in X1 ; :: thesis: t in X2
then ex G being _Graph st
( G in S & t = the_Target_of G ) by A15;
hence t in X2 by A16; :: thesis: verum

end;

assume t in X2 ; :: thesis: t in X1
then ex G being _Graph st
( G in S & t = the_Target_of G ) by A16;
hence t in X1 by A15; :: thesis: verum

end;

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