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

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

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

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

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

end;

assume t in { (the_Target_of G) where G is Element of S : verum } ; :: thesis: t in the_Target_of S
then consider G being Element of S such that
A4: t = the_Target_of G ;
thus t in the_Target_of S by A4, Def17; :: thesis: verum

end;

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