theorem Th67: :: LEXBFS:67

for G being _finite _Graph
for m, n being Nat st G .order() <= m & m <= n holds
(MCS:CSeq G) . m = (MCS:CSeq G) . n