theorem Th34: :: GLIB_004:34

for G being _finite real-weighted WGraph
for i, j being Nat st i <= j holds
( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . j) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . j) `2 )