let G be finite _Graph; :: thesis: for L being LexBFS: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),1 -bag <= ((L `2 ) . (LexBFS:PickUnnumbered L)),1 -bag , InvLexOrder NAT
let L be LexBFS:Labeling of G; :: thesis: for x being set st not x in dom (L `1 ) & dom (L `1 ) <> the_Vertices_of G holds
((L `2 ) . x),1 -bag <= ((L `2 ) . (LexBFS:PickUnnumbered L)),1 -bag , InvLexOrder NAT
let x be set ; :: thesis: ( not x in dom (L `1 ) & dom (L `1 ) <> the_Vertices_of G implies ((L `2 ) . x),1 -bag <= ((L `2 ) . (LexBFS:PickUnnumbered L)),1 -bag , InvLexOrder NAT )
assume that
A1: not x in dom (L `1 ) and
A3: dom (L `1 ) <> the_Vertices_of G ; :: thesis: ((L `2 ) . x),1 -bag <= ((L `2 ) . (LexBFS:PickUnnumbered L)),1 -bag , InvLexOrder NAT
set w = LexBFS:PickUnnumbered L;
set VLG = L `1 ;
set V2G = L `2 ;
set VG = the_Vertices_of G;
A2: dom (L `2 ) = the_Vertices_of G by FUNCT_2:def 1;
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
A6: for x being finite Subset of NAT st x in S holds
x,1 -bag in B and
A7: 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
A8: LexBFS:PickUnnumbered L = choose (F " {(support (max B,(InvLexOrder NAT )))}) by A3, 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
A9: ( y in S & max B,(InvLexOrder NAT ) = y,1 -bag ) by A7;
A10: y = support (max B,(InvLexOrder NAT )) by A9, UPROOTS:10;
then not F " {(support (max B,(InvLexOrder NAT )))} is empty by A4, A9, FUNCT_1:142;
then A11: ( LexBFS:PickUnnumbered L in dom F & F . (LexBFS:PickUnnumbered L) in {(support (max B,(InvLexOrder NAT )))} ) by A8, FUNCT_1:def 13;
then (L `2 ) . (LexBFS:PickUnnumbered L) = F . (LexBFS:PickUnnumbered L) by A5, FUNCT_1:70;
then A12: ((L `2 ) . (LexBFS:PickUnnumbered L)),1 -bag = max B,(InvLexOrder NAT ) by A9, A10, A11, TARSKI:def 1;
A13: dom F = (dom (L `2 )) /\ ((the_Vertices_of G) \ (dom (L `1 ))) by A5, RELAT_1:90;

per cases ( x in the_Vertices_of G or not x in the_Vertices_of G ) ;

suppose x in the_Vertices_of G ; :: thesis: ((L `2 ) . x),1 -bag <= ((L `2 ) . (LexBFS:PickUnnumbered L)),1 -bag , InvLexOrder NAT

then x in (the_Vertices_of G) \ (dom (L `1 )) by A1, XBOOLE_0:def 5;
then A14: x in dom F by A2, A13, XBOOLE_0:def 4;
then A15: F . x = (L `2 ) . x by A5, FUNCT_1:70;
F . x in S by A4, A14, FUNCT_1:def 5;
then ((L `2 ) . x),1 -bag in B by A6, A15;
hence ((L `2 ) . x),1 -bag <= ((L `2 ) . (LexBFS:PickUnnumbered L)),1 -bag , InvLexOrder NAT by A12, Def5; :: thesis: verum

end;

suppose not x in the_Vertices_of G ; :: thesis: ((L `2 ) . x),1 -bag <= ((L `2 ) . (LexBFS:PickUnnumbered L)),1 -bag , InvLexOrder NAT

then (L `2 ) . x = {} by A2, FUNCT_1:def 4;
then ((L `2 ) . x),1 -bag = EmptyBag NAT by UPROOTS:11;
hence ((L `2 ) . x),1 -bag <= ((L `2 ) . (LexBFS:PickUnnumbered L)),1 -bag , InvLexOrder NAT by TERMORD:9; :: thesis: verum

end;

end;