theorem Th74: :: LEXBFS:74

for G being finite _Graph
for n being Nat st n < G .order() holds
((MCS:CSeq G) ``1) .PickedAt n = MCS:PickUnnumbered ((MCS:CSeq G) . n)