let G1 be _finite Tree-like _Graph; :: thesis: for G2 being spanning Tree-like Subgraph of G1 holds G1 == G2
let G2 be spanning Tree-like Subgraph of G1; :: thesis: G1 == G2
G1 .order() = G2 .order() by Th11;
then (G1 .size()) + 1 = G2 .order() by GLIB_002:47;
then (G1 .size()) + 1 = (G2 .size()) + 1 by GLIB_002:47;
hence G1 == G2 by Th13; :: thesis: verum