let G be finite _Graph; :: thesis: for m, n being Nat st G .order() <= m & m <= n holds
(MCS:CSeq G) . m = (MCS:CSeq G) . n
let m, n be Nat; :: thesis: ( G .order() <= m & m <= n implies (MCS:CSeq G) . m = (MCS:CSeq G) . n )
assume A1: ( G .order() <= m & m <= n ) ; :: thesis: (MCS:CSeq G) . m = (MCS:CSeq G) . n
(MCS:CSeq G) . m = (MCS:CSeq G) . (G .order() ) by A1, Th83;
hence (MCS:CSeq G) . m = (MCS:CSeq G) . n by A1, Th83, XXREAL_0:2; :: thesis: verum