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 A1: ( G .order() <= m & m <= n ) ; :: thesis: (LexBFS:CSeq G) . m = (LexBFS:CSeq G) . n
(LexBFS:CSeq G) . m = (LexBFS:CSeq G) . (G .order() ) by A1, Th47;
hence (LexBFS:CSeq G) . m = (LexBFS:CSeq G) . n by A1, Th47, XXREAL_0:2; :: thesis: verum