:: deftheorem defines PRIM:Init GLIB_004:def 14 :
for G being real-weighted WGraph holds PRIM:Init G = [{ the Element of the_Vertices_of G},{}];