:: deftheorem Def17 defines the_Target_of GLIB_014:def 17 :
for S being Graph-membered set
for b₂ being set holds
( b₂ = the_Target_of S iff for t being object holds
( t in b₂ iff ex G being _Graph st
( G in S & t = the_Target_of G ) ) );