per cases ( S is empty or not S is empty ) ;

suppose A13: S is empty ; :: thesis: ex b₁ being set st
for t being object holds
( t in b₁ iff ex G being _Graph st
( G in S & t = the_Target_of G ) )

take the empty set ; :: thesis: for t being object holds
( t in the empty set iff ex G being _Graph st
( G in S & t = the_Target_of G ) )
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: verum

end;

suppose not S is empty ; :: thesis: ex b₁ being set st
for t being object holds
( t in b₁ iff ex G being _Graph st
( G in S & t = the_Target_of G ) )

then reconsider S0 = S as non empty Graph-membered set ;
take X = { (the_Target_of G) where G is Element of S0 : verum } ; :: thesis: for t being object holds
( t in X iff ex G being _Graph st
( G in S & t = the_Target_of G ) )
let t be object ; :: thesis: ( t in X iff ex G being _Graph st
( G in S & t = the_Target_of G ) )

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

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

end;

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

end;

end;