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 A1: dom (L `1) <> the_Vertices_of G ; :: thesis: not MCS:PickUnnumbered L in dom (L `1)

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

A2: S = rng F and

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

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

set y = max S;

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

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

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

assume MCS:PickUnnumbered L in dom (L `1) ; :: thesis: contradiction

then A6: not MCS:PickUnnumbered L in (the_Vertices_of G) \ (dom (L `1)) by XBOOLE_0:def 5;

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

hence contradiction by A5, A6, XBOOLE_0:def 4; :: thesis: verum

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 A1: dom (L `1) <> the_Vertices_of G ; :: thesis: not MCS:PickUnnumbered L in dom (L `1)

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

A2: S = rng F and

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

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

set y = max S;

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

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

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

assume MCS:PickUnnumbered L in dom (L `1) ; :: thesis: contradiction

then A6: not MCS:PickUnnumbered L in (the_Vertices_of G) \ (dom (L `1)) by XBOOLE_0:def 5;

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

hence contradiction by A5, A6, XBOOLE_0:def 4; :: thesis: verum