:: deftheorem defines PRIM:MST GLIB_004:def 18 :
for G being real-weighted WGraph holds PRIM:MST G = (PRIM:CompSeq G) .Result() ;