let G1, G2 be _Graph; :: thesis: for t1 being TColoring of G1
for t2 being TColoring of G2 st G1 == G2 & t1 = t2 & t1 is proper holds
t2 is proper
let t1 be TColoring of G1; :: thesis: for t2 being TColoring of G2 st G1 == G2 & t1 = t2 & t1 is proper holds
t2 is proper
let t2 be TColoring of G2; :: thesis: ( G1 == G2 & t1 = t2 & t1 is proper implies t2 is proper )
assume A1: ( G1 == G2 & t1 = t2 & t1 is proper ) ; :: thesis: t2 is proper
then A2: t2 _V is proper by Th16;
A3: t2 _E is proper by A1, Th90;

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

let e, v, w be object ; :: thesis: ( e Joins v,w,G2 implies (t2 _V) . v <> (t2 _E) . e )
assume e Joins v,w,G2 ; :: thesis: (t2 _V) . v <> (t2 _E) . e
then e Joins v,w,G1 by A1, GLIB_000:88;
hence (t2 _V) . v <> (t2 _E) . e by A1, Th146; :: thesis: verum

end;

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