let G be _finite _Graph; :: thesis: MCS:CSeq G is iterative
set CS = MCS:CSeq G;
let k, n be Nat; :: according to LEXBFS:def 6 :: thesis: ( (MCS:CSeq G) . k = (MCS:CSeq G) . n implies (MCS:CSeq G) . (k + 1) = (MCS:CSeq G) . (n + 1) )
(MCS:CSeq G) . (k + 1) = MCS:Step ((MCS:CSeq G) . k) by Def25;
hence ( (MCS:CSeq G) . k = (MCS:CSeq G) . n implies (MCS:CSeq G) . (k + 1) = (MCS:CSeq G) . (n + 1) ) by Def25; :: thesis: verum