theorem Th75: :: LEXBFS:75

for G being finite _Graph
for n being Nat st n < G .order() holds
ex w being Vertex of G st
( w = MCS:PickUnnumbered ((MCS:CSeq G) . n) & ( for v being set holds
( ( v in G .AdjacentSet {w} & not v in dom (((MCS:CSeq G) . n) `1) implies (((MCS:CSeq G) . (n + 1)) `2) . v = ((((MCS:CSeq G) . n) `2) . v) + 1 ) & ( ( not v in G .AdjacentSet {w} or v in dom (((MCS:CSeq G) . n) `1) ) implies (((MCS:CSeq G) . (n + 1)) `2) . v = (((MCS:CSeq G) . n) `2) . v ) ) ) )