:: deftheorem Def19 defines MCS:PickUnnumbered LEXBFS:def 20 :
for G being _finite _Graph
for L being MCS:Labeling of G
for b₃ being Vertex of G holds
( ( dom (L `1) = the_Vertices_of G implies ( b<sub>3</sub> = MCS:PickUnnumbered L iff b<sub>3</sub> = the Element of the_Vertices_of G ) ) & ( not dom (L `1) = the_Vertices_of G implies ( b₃ = MCS:PickUnnumbered L iff ex S being non empty natural-membered finite set ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b₃ = the Element of F " {(max S)} ) ) ) );