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: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 Lm9;
then A1: the_Vertices_of IT = ((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan() )) `1 by GLIB_000:def 39;
PRIM:MST G = (PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan() ) ;
then ((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan() )) `1 = the_Vertices_of G by Lm18;
hence IT is spanning by A1, GLIB_000:def 35; :: thesis: IT is Tree-like
thus IT is Tree-like by Lm17; :: thesis: verum