theorem Th69: :: LEXBFS:69

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