:: deftheorem defines the_Source_of GLIB_014:def 20 :
for S being non empty Graph-membered set holds the_Source_of S = { (the_Source_of G) where G is Element of S : verum } ;