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