let G be _finite _Graph; 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; 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 ; ( 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
; (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;