:: deftheorem defines the_Weight_of GLIB_003:def 7 :
for G being WGraph holds the_Weight_of G = G . WeightSelector;