let a, b be Real; :: thesis: for n being Nat st a < b holds
( a <= b - ((b - a) / (n + 1)) & b - ((b - a) / (n + 1)) < b & a < a + ((b - a) / (n + 1)) & a + ((b - a) / (n + 1)) <= b )
let n be Nat; :: thesis: ( a < b implies ( a <= b - ((b - a) / (n + 1)) & b - ((b - a) / (n + 1)) < b & a < a + ((b - a) / (n + 1)) & a + ((b - a) / (n + 1)) <= b ) )
assume a < b ; :: thesis: ( a <= b - ((b - a) / (n + 1)) & b - ((b - a) / (n + 1)) < b & a < a + ((b - a) / (n + 1)) & a + ((b - a) / (n + 1)) <= b )
then A1: ( 0 < b - a & 0 < n + 1 ) by XREAL_1:50;
then A2: (b - a) / (n + 1) <= (b - a) / 1 by NAT_1:11, XREAL_1:118;
then a + ((b - a) / (n + 1)) <= b by XREAL_1:19;
hence ( a <= b - ((b - a) / (n + 1)) & b - ((b - a) / (n + 1)) < b ) by A1, XREAL_1:19, XREAL_1:44; :: thesis: ( a < a + ((b - a) / (n + 1)) & a + ((b - a) / (n + 1)) <= b )
thus ( a < a + ((b - a) / (n + 1)) & a + ((b - a) / (n + 1)) <= b ) by A1, A2, XREAL_1:19, XREAL_1:29; :: thesis: verum