let G be _Graph; :: thesis: for t being TColoring of G
for H being Subgraph of G
for t9 being TColoring of H st t9 = [((t _V) | (the_Vertices_of H)),((t _E) | (the_Edges_of H))] & t is proper holds
t9 is proper
let t be TColoring of G; :: thesis: for H being Subgraph of G
for t9 being TColoring of H st t9 = [((t _V) | (the_Vertices_of H)),((t _E) | (the_Edges_of H))] & t is proper holds
t9 is proper
let H be Subgraph of G; :: thesis: for t9 being TColoring of H st t9 = [((t _V) | (the_Vertices_of H)),((t _E) | (the_Edges_of H))] & t is proper holds
t9 is proper
let t9 be TColoring of H; :: thesis: ( t9 = [((t _V) | (the_Vertices_of H)),((t _E) | (the_Edges_of H))] & t is proper implies t9 is proper )
assume A1: ( t9 = [((t _V) | (the_Vertices_of H)),((t _E) | (the_Edges_of H))] & t is proper ) ; :: thesis: t9 is proper
then A2: t9 _V is proper by Th15;
A3: t9 _E is proper by A1, Th89;

now :: thesis: for e, v, w being object st e Joins v,w,H holds
(t9 _V) . v <> (t9 _E) . e

let e, v, w be object ; :: thesis: ( e Joins v,w,H implies (t9 _V) . v <> (t9 _E) . e )
assume A4: e Joins v,w,H ; :: thesis: (t9 _V) . v <> (t9 _E) . e
then ( e in the_Edges_of H & v in the_Vertices_of H ) by GLIB_000:def 13, GLIB_000:13;
then A5: ( e in dom (t9 _E) & v in dom (t9 _V) ) by PARTFUN1:def 2;
( v is set & w is set ) by TARSKI:1;
then e Joins v,w,G by A4, GLIB_000:72;
then A6: (t _V) . v <> (t _E) . e by A1, Th146;
( (t _V) . v = (t9 _V) . v & (t _E) . e = (t9 _E) . e ) by A1, A5, FUNCT_1:47;
hence (t9 _V) . v <> (t9 _E) . e by A6; :: thesis: verum

end;

hence t9 is proper by A2, A3, Th146; :: thesis: verum