theorem Th65: :: LEXBFS:65

for G being _finite _Graph
for n being Nat st n <= G .order() holds
card (dom (((MCS:CSeq G) . n) `1)) = n