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

A2: dom (L `1) <> the_Vertices_of G ; :: thesis: (((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;

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

A2: dom (L `1) <> the_Vertices_of G ; :: thesis: (((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 )
;

end;

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 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; :: thesis: verum

end;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; :: thesis: verum

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 A15, FUNCT_1:def 2;

then (((L `2) . x),1) -bag = EmptyBag NAT by UPROOTS:9;

hence (((L `2) . x),1) -bag <= (((L `2) . (LexBFS:PickUnnumbered L)),1) -bag , InvLexOrder NAT by TERMORD:9; :: thesis: verum

end;then (((L `2) . x),1) -bag = EmptyBag NAT by UPROOTS:9;

hence (((L `2) . x),1) -bag <= (((L `2) . (LexBFS:PickUnnumbered L)),1) -bag , InvLexOrder NAT by TERMORD:9; :: thesis: verum