let G be _finite _Graph; :: thesis: for L being MCS: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 <= (L `2) . (MCS:PickUnnumbered L)

let L be MCS: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 <= (L `2) . (MCS:PickUnnumbered L)

let x be set ; :: thesis: ( not x in dom (L `1) & dom (L `1) <> the_Vertices_of G implies (L `2) . x <= (L `2) . (MCS:PickUnnumbered L) )

assume that

A1: not x in dom (L `1) and

A2: dom (L `1) <> the_Vertices_of G ; :: thesis: (L `2) . x <= (L `2) . (MCS:PickUnnumbered L)

set VG = the_Vertices_of G;

set V2G = L `2 ;

set VLG = L `1 ;

set w = MCS:PickUnnumbered L;

consider S being non empty natural-membered finite set , F being Function such that

A3: S = rng F and

A4: F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) and

A5: MCS:PickUnnumbered L = the Element of F " {(max S)} by A2, Def19;

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

set y = max S;

max S in rng F by A3, XXREAL_2:def 8;

then A7: not F " {(max S)} is empty by FUNCT_1:72;

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

then A8: (L `2) . (MCS:PickUnnumbered L) = F . (MCS:PickUnnumbered L) by A4, FUNCT_1:47;

F . (MCS:PickUnnumbered L) in {(max S)} by A5, A7, FUNCT_1:def 7;

then A9: (L `2) . (MCS:PickUnnumbered L) = max S by A8, TARSKI:def 1;

A10: 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 <= (L `2) . (MCS:PickUnnumbered L)

let L be MCS: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 <= (L `2) . (MCS:PickUnnumbered L)

let x be set ; :: thesis: ( not x in dom (L `1) & dom (L `1) <> the_Vertices_of G implies (L `2) . x <= (L `2) . (MCS:PickUnnumbered L) )

assume that

A1: not x in dom (L `1) and

A2: dom (L `1) <> the_Vertices_of G ; :: thesis: (L `2) . x <= (L `2) . (MCS:PickUnnumbered L)

set VG = the_Vertices_of G;

set V2G = L `2 ;

set VLG = L `1 ;

set w = MCS:PickUnnumbered L;

consider S being non empty natural-membered finite set , F being Function such that

A3: S = rng F and

A4: F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) and

A5: MCS:PickUnnumbered L = the Element of F " {(max S)} by A2, Def19;

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

set y = max S;

max S in rng F by A3, XXREAL_2:def 8;

then A7: not F " {(max S)} is empty by FUNCT_1:72;

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

then A8: (L `2) . (MCS:PickUnnumbered L) = F . (MCS:PickUnnumbered L) by A4, FUNCT_1:47;

F . (MCS:PickUnnumbered L) in {(max S)} by A5, A7, FUNCT_1:def 7;

then A9: (L `2) . (MCS:PickUnnumbered L) = max S by A8, TARSKI:def 1;

A10: 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 <= (L `2) . (MCS:PickUnnumbered L)

then
x in (the_Vertices_of G) \ (dom (L `1))
by A1, XBOOLE_0:def 5;

then A11: x in dom F by A10, A6, XBOOLE_0:def 4;

then A12: F . x in S by A3, FUNCT_1:def 3;

F . x = (L `2) . x by A4, A11, FUNCT_1:47;

hence (L `2) . x <= (L `2) . (MCS:PickUnnumbered L) by A9, A12, XXREAL_2:def 8; :: thesis: verum

end;then A11: x in dom F by A10, A6, XBOOLE_0:def 4;

then A12: F . x in S by A3, FUNCT_1:def 3;

F . x = (L `2) . x by A4, A11, FUNCT_1:47;

hence (L `2) . x <= (L `2) . (MCS:PickUnnumbered L) by A9, A12, XXREAL_2:def 8; :: thesis: verum