let G be finite _Graph; :: thesis:
let L be MCS:Labeling of G; :: thesis:
let x be set ; :: thesis:
assume that
A1: not x in dom (L `1 ) and
A3: dom (L `1 ) <> the_Vertices_of G ; :: thesis:
A2: dom (L `2 ) = the_Vertices_of G by FUNCT_2:def 1;
set w = MCS:PickUnnumbered L;
set VLG = L `1 ;
set V2G = L `2 ;
set VG = the_Vertices_of G;
consider S being non empty natural-membered finite set , F being Function such that
A4: S = rng F and
A5: F = (L `2 ) | ((the_Vertices_of G) \ (dom (L `1 ))) and
A6: MCS:PickUnnumbered L = choose (F " {(max S)}) by A3, Def36;
set y = max S;
max S in rng F by A4, XXREAL_2:def 8;
then not F " {(max S)} is empty by FUNCT_1:142;
then A7: ( MCS:PickUnnumbered L in dom F & F . (MCS:PickUnnumbered L) in {(max S)} ) by A6, FUNCT_1:def 13;
then (L `2 ) . (MCS:PickUnnumbered L) = F . (MCS:PickUnnumbered L) by A5, FUNCT_1:70;
then A8: (L `2 ) . (MCS:PickUnnumbered L) = max S by A7, TARSKI:def 1;
A9: dom F = (dom (L `2 )) /\ ((the_Vertices_of G) \ (dom (L `1 ))) by A5, RELAT_1:90;

per cases ;

suppose x in the_Vertices_of G ; :: thesis:

then x in (the_Vertices_of G) \ (dom (L `1 )) by A1, XBOOLE_0:def 5;
then A10: x in dom F by A2, A9, XBOOLE_0:def 4;
then A11: F . x = (L `2 ) . x by A5, FUNCT_1:70;
F . x in S by A4, A10, FUNCT_1:def 5;
hence (L `2 ) . x <= (L `2 ) . (MCS:PickUnnumbered L) by A8, A11, XXREAL_2:def 8; :: thesis:

end;

suppose not x in the_Vertices_of G ; :: thesis:

hence (L `2 ) . x <= (L `2 ) . (MCS:PickUnnumbered L) by A2, FUNCT_1:def 4; :: thesis:

end;