theorem Th59: :: LEXBFS:59

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