:: deftheorem defines LexBFS:Init LEXBFS:def 11 :
for G being _Graph holds LexBFS:Init G = [{},((the_Vertices_of G) --> {})];