:: deftheorem defines -TVSet GRAPH_4:def 4 :
for G being Graph
for X being set holds G -TVSet X = { v where v is Element of G : ex e being Element of the carrier' of G st
( e in X & v = the Target of G . e ) } ;