let G1, G2 be _Graph; :: thesis: ( G1 == G2 & G1 is Tree-like implies G2 is Tree-like )
assume A1: ( G1 == G2 & G1 is Tree-like ) ; :: thesis: G2 is Tree-like
( G2 is connected & G2 is acyclic ) by A1, Th8, Th44;
hence G2 is Tree-like ; :: thesis: verum