let G1, G2 be _Graph; :: thesis: for x being set st G1 == G2 & G1 is_DTree_rooted_at x holds
G2 is_DTree_rooted_at x
let x be set ; :: thesis: ( G1 == G2 & G1 is_DTree_rooted_at x implies G2 is_DTree_rooted_at x )
assume that
A1: G1 == G2 and
A2: G1 is_DTree_rooted_at x ; :: thesis: G2 is_DTree_rooted_at x
A3: now :: thesis: for y being Vertex of G2 ex W9 being DWalk of G2 st W9 is_Walk_from x,y
let y be Vertex of G2; :: thesis: ex W9 being DWalk of G2 st W9 is_Walk_from x,y
reconsider y9 = y as Vertex of G1 by A1, GLIB_000:def 34;
consider W being DWalk of G1 such that
A4: W is_Walk_from x,y9 by A2;
reconsider W9 = W as DWalk of G2 by A1, GLIB_001:179, GLIB_001:181;
take W9 = W9; :: thesis: W9 is_Walk_from x,y
thus W9 is_Walk_from x,y by A4, GLIB_001:19; :: thesis: verum
end;
G1 is Tree-like by A2;
then G2 is Tree-like by A1, Th47;
hence G2 is_DTree_rooted_at x by A3; :: thesis: verum