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 that
A1: G .order() <= m and
A2: m <= n ; :: thesis: (MCS:CSeq G) . m = (MCS:CSeq G) . n
(MCS:CSeq G) . m = (MCS:CSeq G) . (G .order()) by A1, Th66;
hence (MCS:CSeq G) . m = (MCS:CSeq G) . n by A1, A2, Th66, XXREAL_0:2; :: thesis: verum