let k be Nat; :: thesis: for t being 1 _greater Nat holds [.0,((k + 1) / t).[ \/ [.((k + 1) / t),((k + 2) / t).[ = [.0,((k + 2) / t).[
let t be 1 _greater Nat; :: thesis: [.0,((k + 1) / t).[ \/ [.((k + 1) / t),((k + 2) / t).[ = [.0,((k + 2) / t).[
( 0 <= (k + 1) / t & (k + 1) / t <= (k + 2) / t )

proof

k + 1 <= (k + 1) + 1 by XREAL_1:31;
hence ( 0 <= (k + 1) / t & (k + 1) / t <= (k + 2) / t ) by XREAL_1:64; :: thesis: verum

end;

hence [.0,((k + 1) / t).[ \/ [.((k + 1) / t),((k + 2) / t).[ = [.0,((k + 2) / t).[ by XXREAL_1:168; :: thesis: verum