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 = the Element of F " {(support (max (B,(InvLexOrder NAT))))}
by A2, Def11;
A8:
dom F = (dom (L `2)) /\ ((the_Vertices_of G) \ (dom (L `1)))
by A4, RELAT_1:61;
set mw = max (B,(InvLexOrder NAT));
max (B,(InvLexOrder NAT)) in B
by Def4;
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:8;
then A12:
not F " {(support (max (B,(InvLexOrder NAT))))} is empty
by A3, A9, FUNCT_1:72;
then
LexBFS:PickUnnumbered L in dom F
by A7, FUNCT_1:def 7;
then A13:
(L `2) . (LexBFS:PickUnnumbered L) = F . (LexBFS:PickUnnumbered L)
by A4, FUNCT_1:47;
F . (LexBFS:PickUnnumbered L) in {(support (max (B,(InvLexOrder NAT))))}
by A7, A12, FUNCT_1:def 7;
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 NATthen
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 3;
F . x = (L `2) . x
by A4, A16, FUNCT_1:47;
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, Def4;
verum end;