:: deftheorem Def16 defines the_Source_of GLIB_014:def 16 :
for S being Graph-membered set
for b₂ being set holds
( b₂ = the_Source_of S iff for s being object holds
( s in b₂ iff ex G being _Graph st
( G in S & s = the_Source_of G ) ) );