A1: for n, k being Element of NAT st n < k holds
bq . n < bq . k

proof

let n, k be Element of NAT ; :: thesis: ( n < k implies bq . n < bq . k )
assume A2: n < k ; :: thesis: bq . n < bq . k
A3: 2 * n < 2 * k by A2, XREAL_1:70;
A4: (2 * n) + 1 < (2 * k) + 1 by A3, XREAL_1:8;
A5: bq . n < (2 * k) + 1 by A4, Lm6;
thus bq . n < bq . k by A5, Lm6; :: thesis: verum

end;

A6: for n being Element of NAT holds bq . n is Element of NAT

proof

let n be Element of NAT ; :: thesis: bq . n is Element of NAT
A7: (2 * n) + 1 is Element of NAT ;
thus bq . n is Element of NAT by A7, Lm6; :: thesis: verum

end;

thus bq is increasing sequence of NAT by A1, A6, SEQM_3:7, SEQM_3:29; :: thesis: verum