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
A2: dom (L `1 ) <> the_Vertices_of G ; :: thesis:
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 = choose (F " {(max S)}) by A2, Def20;
A6: dom F = (dom (L `2 )) /\ ((the_Vertices_of G) \ (dom (L `1 ))) by A4, RELAT_1:90;
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:142;
then MCS:PickUnnumbered L in dom F by A5, FUNCT_1:def 13;
then A8: (L `2 ) . (MCS:PickUnnumbered L) = F . (MCS:PickUnnumbered L) by A4, FUNCT_1:70;
F . (MCS:PickUnnumbered L) in {(max S)} by A5, A7, FUNCT_1:def 13;
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;

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 A11: x in dom F by A10, A6, XBOOLE_0:def 4;
then A12: F . x in S by A3, FUNCT_1:def 5;
F . x = (L `2 ) . x by A4, A11, FUNCT_1:70;
hence (L `2 ) . x <= (L `2 ) . (MCS:PickUnnumbered L) by A9, A12, 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 A10, FUNCT_1:def 4; :: thesis:

end;

end;