let G be _Graph; :: thesis: for f being VColoring of G
for g being EColoring of G st g is proper holds
ex g9 being proper EColoring of G st
( rng f misses rng g9 & card (rng g) = card (rng g9) )
let f be VColoring of G; :: thesis: for g being EColoring of G st g is proper holds
ex g9 being proper EColoring of G st
( rng f misses rng g9 & card (rng g) = card (rng g9) )
let g be EColoring of G; :: thesis: ( g is proper implies ex g9 being proper EColoring of G st
( rng f misses rng g9 & card (rng g) = card (rng g9) ) )
assume A1: g is proper ; :: thesis: ex g9 being proper EColoring of G st
( rng f misses rng g9 & card (rng g) = card (rng g9) )
set h = <:((rng g) --> (rng f)),(id (rng g)):>;
set g9 = <:((rng g) --> (rng f)),(id (rng g)):> * g;
A2: dom <:((rng g) --> (rng f)),(id (rng g)):> = rng g by Lm8;
then reconsider g9 = <:((rng g) --> (rng f)),(id (rng g)):> * g as EColoring of G by Th77;
reconsider g9 = g9 as proper EColoring of G by A1, Th87;
take g9 ; :: thesis: ( rng f misses rng g9 & card (rng g) = card (rng g9) )
A3: rng g9 = rng <:((rng g) --> (rng f)),(id (rng g)):> by A2, RELAT_1:28;
hence rng f misses rng g9 by Lm11; :: thesis: card (rng g) = card (rng g9)
thus card (rng g) = card [:(rng g),{(rng f)}:] by CARD_1:69
.= card [:{(rng f)},(rng g):] by CARD_2:4
.= card (rng g9) by A3, Lm10 ; :: thesis: verum