:: deftheorem Def11 defines LexBFS:PickUnnumbered LEXBFS:def 12 :
for G being _finite _Graph
for L being LexBFS:Labeling of G
for b₃ being Vertex of G holds
( ( dom (L `1) = the_Vertices_of G implies ( b<sub>3</sub> = LexBFS:PickUnnumbered L iff b<sub>3</sub> = the Element of the_Vertices_of G ) ) & ( not dom (L `1) = the_Vertices_of G implies ( b₃ = LexBFS:PickUnnumbered L iff ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & b₃ = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) ) ) );