let G2 be _Graph; :: thesis: for v being object
for V being finite set
for G1 being addAdjVertexAll of G2,v,V holds
( G1 is finite-ecolorable iff G2 is finite-ecolorable )
let v be object ; :: thesis: for V being finite set
for G1 being addAdjVertexAll of G2,v,V holds
( G1 is finite-ecolorable iff G2 is finite-ecolorable )
let V be finite set ; :: thesis: for G1 being addAdjVertexAll of G2,v,V holds
( G1 is finite-ecolorable iff G2 is finite-ecolorable )
let G1 be addAdjVertexAll of G2,v,V; :: thesis: ( G1 is finite-ecolorable iff G2 is finite-ecolorable )

hereby :: thesis: ( G2 is finite-ecolorable implies G1 is finite-ecolorable )

assume A1: G1 is finite-ecolorable ; :: thesis: G2 is finite-ecolorable
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is finite-ecolorable by A1; :: thesis: verum

end;

assume G2 is finite-ecolorable ; :: thesis: G1 is finite-ecolorable
then consider n being Nat such that
A2: G2 is n -ecolorable ;
reconsider G2 = G2 as n -ecolorable _Graph by A2;
G1 is addAdjVertexAll of G2,v,V ;
hence G1 is finite-ecolorable ; :: thesis: verum