let G be finite _Graph; :: thesis: for L being LexBFS:Labeling of G st dom (L `1 ) <> the_Vertices_of G holds
not LexBFS:PickUnnumbered L in dom (L `1 )
let L be LexBFS:Labeling of G; :: thesis: ( dom (L `1 ) <> the_Vertices_of G implies not LexBFS:PickUnnumbered L in dom (L `1 ) )
assume A2: dom (L `1 ) <> the_Vertices_of G ; :: thesis: not LexBFS:PickUnnumbered L in dom (L `1 )
set w = LexBFS:PickUnnumbered L;
set VLG = L `1 ;
set V2G = L `2 ;
set VG = the_Vertices_of G;
assume A3: LexBFS:PickUnnumbered L in dom (L `1 ) ; :: thesis: contradiction
consider S being non empty finite Subset of (bool NAT ), B being non empty finite Subset of (Bags NAT ), F being Function such that
A4: S = rng F and
A5: F = (L `2 ) | ((the_Vertices_of G) \ (dom (L `1 ))) and
for x being finite Subset of NAT st x in S holds
x,1 -bag in B and
A6: for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = y,1 -bag ) and
A7: LexBFS:PickUnnumbered L = choose (F " {(support (max B,(InvLexOrder NAT )))}) by A2, Def29;
set mw = max B,(InvLexOrder NAT );
max B,(InvLexOrder NAT ) in B by Def5;
then consider y being finite Subset of NAT such that
A8: ( y in S & max B,(InvLexOrder NAT ) = y,1 -bag ) by A6;
y = support (max B,(InvLexOrder NAT )) by A8, UPROOTS:10;
then not F " {(support (max B,(InvLexOrder NAT )))} is empty by A4, A8, FUNCT_1:142;
then A9: LexBFS:PickUnnumbered L in dom F by A7, FUNCT_1:def 13;
A10: dom F = (dom (L `2 )) /\ ((the_Vertices_of G) \ (dom (L `1 ))) by A5, RELAT_1:90;
not LexBFS:PickUnnumbered L in (the_Vertices_of G) \ (dom (L `1 )) by A3, XBOOLE_0:def 5;
hence contradiction by A9, A10, XBOOLE_0:def 4; :: thesis: verum