let X be set ; :: thesis: ( X = the_Source_of S iff X = { (the_Source_of G) where G is Element of S : verum } )
set Y = { (the_Source_of G) where G is Element of S : verum } ;

now :: thesis: for s being object holds
( ( s in the_Source_of S implies s in { (the_Source_of G) where G is Element of S : verum } ) & ( s in { (the_Source_of G) where G is Element of S : verum } implies s in the_Source_of S ) )

let s be object ; :: thesis: ( ( s in the_Source_of S implies s in { (the_Source_of G) where G is Element of S : verum } ) & ( s in { (the_Source_of G) where G is Element of S : verum } implies s in the_Source_of S ) )

hereby :: thesis: ( s in { (the_Source_of G) where G is Element of S : verum } implies s in the_Source_of S )

assume s in the_Source_of S ; :: thesis: s in { (the_Source_of G) where G is Element of S : verum }
then ex G being _Graph st
( G in S & s = the_Source_of G ) by Def16;
hence s in { (the_Source_of G) where G is Element of S : verum } ; :: thesis: verum

end;

assume s in { (the_Source_of G) where G is Element of S : verum } ; :: thesis: s in the_Source_of S
then consider G being Element of S such that
A3: s = the_Source_of G ;
thus s in the_Source_of S by A3, Def16; :: thesis: verum

end;

hence ( X = the_Source_of S iff X = { (the_Source_of G) where G is Element of S : verum } ) by TARSKI:2; :: thesis: verum