let G be _Graph; :: thesis: for g being EColoring of G
for H being Subgraph of G
for g9 being EColoring of H st g9 = g | (the_Edges_of H) & g is proper holds
g9 is proper
let g be EColoring of G; :: thesis: for H being Subgraph of G
for g9 being EColoring of H st g9 = g | (the_Edges_of H) & g is proper holds
g9 is proper
let H be Subgraph of G; :: thesis: for g9 being EColoring of H st g9 = g | (the_Edges_of H) & g is proper holds
g9 is proper
let g9 be EColoring of H; :: thesis: ( g9 = g | (the_Edges_of H) & g is proper implies g9 is proper )
assume A1: ( g9 = g | (the_Edges_of H) & g is proper ) ; :: thesis: g9 is proper

now :: thesis: for v being Vertex of H
for e1, e2 being object st e1 in v .edgesInOut() & e2 in v .edgesInOut() & g9 . e1 = g9 . e2 holds
e1 = e2

let v be Vertex of H; :: thesis: for e1, e2 being object st e1 in v .edgesInOut() & e2 in v .edgesInOut() & g9 . e1 = g9 . e2 holds
e1 = e2
let e1, e2 be object ; :: thesis: ( e1 in v .edgesInOut() & e2 in v .edgesInOut() & g9 . e1 = g9 . e2 implies e1 = e2 )
assume A2: ( e1 in v .edgesInOut() & e2 in v .edgesInOut() & g9 . e1 = g9 . e2 ) ; :: thesis: e1 = e2
( the_Vertices_of H c= the_Vertices_of G & v in the_Vertices_of H ) ;
then reconsider w = v as Vertex of G ;
A3: v .edgesInOut() c= w .edgesInOut() by GLIB_000:78;
( g9 . e1 = g . e1 & g9 . e2 = g . e2 ) by A1, A2, FUNCT_1:49;
hence e1 = e2 by A1, A2, A3, Th85; :: thesis: verum

end;

hence g9 is proper by Th85; :: thesis: verum