A1: for n, k being Nat st n < k holds
bq . n < bq . k

proof

let n, k be Nat; :: thesis: ( n < k implies bq . n < bq . k )
assume n < k ; :: thesis: bq . n < bq . k
then 2 * n < 2 * k by XREAL_1:68;
then (2 * n) + 1 < (2 * k) + 1 by XREAL_1:6;
then bq . n < (2 * k) + 1 by Lm6;
hence bq . n < bq . k by Lm6; :: thesis: verum

end;

for n being Nat holds bq . n is Element of NAT

proof

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

end;

hence bq is increasing sequence of NAT by A1, SEQM_3:1, SEQM_3:13; :: thesis: verum