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
; ( 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; 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; verum