let G be finite _Graph; :: thesis: for L being MCS:Labeling of G st dom (L `1 ) <> the_Vertices_of G holds
not MCS:PickUnnumbered L in dom (L `1 )
let L be MCS:Labeling of G; :: thesis: ( dom (L `1 ) <> the_Vertices_of G implies not MCS:PickUnnumbered L in dom (L `1 ) )
assume A2: dom (L `1 ) <> the_Vertices_of G ; :: thesis: not MCS:PickUnnumbered L in dom (L `1 )
set w = MCS:PickUnnumbered L;
set VLG = L `1 ;
set V2G = L `2 ;
set VG = the_Vertices_of G;
assume A3: MCS:PickUnnumbered L in dom (L `1 ) ; :: thesis: contradiction
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 A2, 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 by A6, FUNCT_1:def 13;
A8: dom F = (dom (L `2 )) /\ ((the_Vertices_of G) \ (dom (L `1 ))) by A5, RELAT_1:90;
not MCS:PickUnnumbered L in (the_Vertices_of G) \ (dom (L `1 )) by A3, XBOOLE_0:def 5;
hence contradiction by A7, A8, XBOOLE_0:def 4; :: thesis: verum