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

(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