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