set PCS = PRIM:CompSeq G;
set n = (PRIM:CompSeq G) .Lifespan() ;
set IT = the inducedWSubgraph of G,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `1 ,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `2 ;
take the inducedWSubgraph of G,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `1 ,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `2 ; :: thesis: ( the inducedWSubgraph of G,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `1 ,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `2 is spanning & the inducedWSubgraph of G,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `1 ,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `2 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;
thus the inducedWSubgraph of G,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `1 ,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `2 is spanning by A1; :: thesis: the inducedWSubgraph of G,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `1 ,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `2 is Tree-like
thus the inducedWSubgraph of G,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `1 ,((PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan())) `2 is Tree-like by Th38; :: thesis: verum