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