let X1, X2 be set ; :: thesis: ( ( for s being object holds
( s in X1 iff ex G being _Graph st
( G in S & s = the_Source_of G ) ) ) & ( for s being object holds
( s in X2 iff ex G being _Graph st
( G in S & s = the_Source_of G ) ) ) implies X1 = X2 )
assume that
A11: for s being object holds
( s in X1 iff ex G being _Graph st
( G in S & s = the_Source_of G ) ) and
A12: for s being object holds
( s in X2 iff ex G being _Graph st
( G in S & s = the_Source_of G ) ) ; :: thesis: X1 = X2

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

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

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

assume s in X1 ; :: thesis: s in X2
then ex G being _Graph st
( G in S & s = the_Source_of G ) by A11;
hence s in X2 by A12; :: thesis: verum

end;

assume s in X2 ; :: thesis: s in X1
then ex G being _Graph st
( G in S & s = the_Source_of G ) by A12;
hence s in X1 by A11; :: thesis: verum

end;

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