let G be finite _Graph; 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; 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 ; ( 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
A2:
dom (L `1 ) <> the_Vertices_of G
; ((L `2 ) . x),1 -bag <= ((L `2 ) . (LexBFS:PickUnnumbered L)),1 -bag , InvLexOrder NAT
set VG = the_Vertices_of G;
set V2G = L `2 ;
set VLG = L `1 ;
set w = LexBFS:PickUnnumbered L;
consider S being non empty finite Subset of (bool NAT ), B being non empty finite Subset of (Bags NAT ), F being Function such that
A3:
S = rng F
and
A4:
F = (L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))
and
A5:
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, Def12;
A8:
dom F = (dom (L `2 )) /\ ((the_Vertices_of G) \ (dom (L `1 )))
by A4, RELAT_1:90;
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
and
A10:
max B,(InvLexOrder NAT ) = y,1 -bag
by A6;
A11:
y = support (max B,(InvLexOrder NAT ))
by A10, UPROOTS:10;
then A12:
not F " {(support (max B,(InvLexOrder NAT )))} is empty
by A3, A9, FUNCT_1:142;
then
LexBFS:PickUnnumbered L in dom F
by A7, FUNCT_1:def 13;
then A13:
(L `2 ) . (LexBFS:PickUnnumbered L) = F . (LexBFS:PickUnnumbered L)
by A4, FUNCT_1:70;
F . (LexBFS:PickUnnumbered L) in {(support (max B,(InvLexOrder NAT )))}
by A7, A12, FUNCT_1:def 13;
then A14:
((L `2 ) . (LexBFS:PickUnnumbered L)),1 -bag = max B,(InvLexOrder NAT )
by A10, A11, A13, TARSKI:def 1;
A15:
dom (L `2 ) = the_Vertices_of G
by FUNCT_2:def 1;
per cases
( x in the_Vertices_of G or not x in the_Vertices_of G )
;
suppose
x in the_Vertices_of G
;
((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 A16:
x in dom F
by A15, A8, XBOOLE_0:def 4;
then A17:
F . x in S
by A3, FUNCT_1:def 5;
F . x = (L `2 ) . x
by A4, A16, FUNCT_1:70;
then
((L `2 ) . x),1
-bag in B
by A5, A17;
hence
((L `2 ) . x),1
-bag <= ((L `2 ) . (LexBFS:PickUnnumbered L)),1
-bag ,
InvLexOrder NAT
by A14, Def5;
verum end;