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

let n, k be Nat; :: thesis:
assume n < k ; :: thesis:
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:

end;

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

end;