let G be _finite _Graph; :: thesis: for m, n being Nat st G .order() <= m & m <= n holds
(LexBFS:CSeq G) . m = (LexBFS:CSeq G) . n
let m, n be Nat; :: thesis: ( G .order() <= m & m <= n implies (LexBFS:CSeq G) . m = (LexBFS:CSeq G) . n )
assume that
A1: G .order() <= m and
A2: m <= n ; :: thesis: (LexBFS:CSeq G) . m = (LexBFS:CSeq G) . n
(LexBFS:CSeq G) . m = (LexBFS:CSeq G) . (G .order()) by A1, Th33;
hence (LexBFS:CSeq G) . m = (LexBFS:CSeq G) . n by A1, A2, Th33, XXREAL_0:2; :: thesis: verum