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 A1: dom (L `1) <> the_Vertices_of G ; :: thesis: not LexBFS:PickUnnumbered L in dom (L `1)

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

A2: S = rng F and

A3: 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

A4: 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

A5: LexBFS:PickUnnumbered L = the Element of F " {(support (max (B,(InvLexOrder NAT))))} by A1, Def11;

set mw = max (B,(InvLexOrder NAT));

max (B,(InvLexOrder NAT)) in B by Def4;

then consider y being finite Subset of NAT such that

A6: y in S and

A7: max (B,(InvLexOrder NAT)) = (y,1) -bag by A4;

y = support (max (B,(InvLexOrder NAT))) by A7, UPROOTS:8;

then not F " {(support (max (B,(InvLexOrder NAT))))} is empty by A2, A6, FUNCT_1:72;

then A8: LexBFS:PickUnnumbered L in dom F by A5, FUNCT_1:def 7;

assume LexBFS:PickUnnumbered L in dom (L `1) ; :: thesis: contradiction

then A9: not LexBFS:PickUnnumbered L in (the_Vertices_of G) \ (dom (L `1)) by XBOOLE_0:def 5;

dom F = (dom (L `2)) /\ ((the_Vertices_of G) \ (dom (L `1))) by A3, RELAT_1:61;

hence contradiction by A8, A9, XBOOLE_0:def 4; :: thesis: verum

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 A1: dom (L `1) <> the_Vertices_of G ; :: thesis: not LexBFS:PickUnnumbered L in dom (L `1)

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

A2: S = rng F and

A3: 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

A4: 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

A5: LexBFS:PickUnnumbered L = the Element of F " {(support (max (B,(InvLexOrder NAT))))} by A1, Def11;

set mw = max (B,(InvLexOrder NAT));

max (B,(InvLexOrder NAT)) in B by Def4;

then consider y being finite Subset of NAT such that

A6: y in S and

A7: max (B,(InvLexOrder NAT)) = (y,1) -bag by A4;

y = support (max (B,(InvLexOrder NAT))) by A7, UPROOTS:8;

then not F " {(support (max (B,(InvLexOrder NAT))))} is empty by A2, A6, FUNCT_1:72;

then A8: LexBFS:PickUnnumbered L in dom F by A5, FUNCT_1:def 7;

assume LexBFS:PickUnnumbered L in dom (L `1) ; :: thesis: contradiction

then A9: not LexBFS:PickUnnumbered L in (the_Vertices_of G) \ (dom (L `1)) by XBOOLE_0:def 5;

dom F = (dom (L `2)) /\ ((the_Vertices_of G) \ (dom (L `1))) by A3, RELAT_1:61;

hence contradiction by A8, A9, XBOOLE_0:def 4; :: thesis: verum