per cases ;

suppose A13: S is empty ; :: thesis:

take the empty set ; :: thesis:
thus for t being object holds
( t in the empty set iff ex G being _Graph st
( G in S & t = the_Target_of G ) ) by A13; :: thesis:

end;

suppose not S is empty ; :: thesis:

then reconsider S0 = S as non empty Graph-membered set ;
take X = { (the_Target_of G) where G is Element of S0 : verum } ; :: thesis:
let t be object ; :: thesis:

hereby :: thesis:

assume t in X ; :: thesis:
then consider G being Element of S0 such that
A14: t = the_Target_of G ;
reconsider G = G as _Graph ;
take G = G; :: thesis:
thus ( G in S & t = the_Target_of G ) by A14; :: thesis:

end;

thus ( ex G being _Graph st
( G in S & t = the_Target_of G ) implies t in X ) ; :: thesis:

end;

end;