set PCS = PRIM:CompSeq G;
set n = (PRIM:CompSeq G) .Lifespan() ;
consider IT being inducedWSubgraph of G,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `1 ,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `2 ;
take IT ; :: thesis: ( IT is spanning & IT is Tree-like )
PRIM:MST G = (PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan()) ;
then A1: ((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `1 = the_Vertices_of G by Th39;
( ((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `2 c= G .edgesBetween (((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `1) ) by Th30;
then the_Vertices_of IT = ((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `1 by GLIB_000:def 39;
hence IT is spanning by A1, GLIB_000:def 35; :: thesis: IT is Tree-like
thus IT is Tree-like by Th38; :: thesis: verum