theorem Th58: :: LEXBFS:58

for G being _finite _Graph
for L being MCS:Labeling of G
for x being set st not x in dom (L `1) & dom (L `1) <> the_Vertices_of G holds
(L `2) . x <= (L `2) . (MCS:PickUnnumbered L)