theorem Th42: :: GLIB_004:42

for G being _finite connected real-weighted WGraph
for n being Nat holds ((PRIM:CompSeq G) . n) `2 c= (PRIM:MST G) `2