theorem Th30: :: LEXBFS:30

for G being _finite _Graph
for L being LexBFS:Labeling of G st dom (L `1) <> the_Vertices_of G holds
not LexBFS:PickUnnumbered L in dom (L `1)