:: deftheorem defines .cost() GLIB_004:def 6 :
for G being finite real-weighted WGraph holds G .cost() = Sum (the_Weight_of G);