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