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

then G2 is Tree-like by A1, Th47;

hence G2 is_DTree_rooted_at x by A3; :: thesis: verum

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

G1 is Tree-like
by A2;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;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

then G2 is Tree-like by A1, Th47;

hence G2 is_DTree_rooted_at x by A3; :: thesis: verum