theorem Th64: :: LEXBFS:64

for G being _finite _Graph
for n being Nat st card (dom (((MCS:CSeq G) . n) `1)) < G .order() holds
((MCS:CSeq G) . (n + 1)) `1 = (((MCS:CSeq G) . n) `1) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order()) -' (card (dom (((MCS:CSeq G) . n) `1)))))