:: deftheorem defines MCS:Init LEXBFS:def 19 :
for G being finite _Graph holds MCS:Init G = [{},((the_Vertices_of G) --> 0)];