theorem Th22: :: MESFUN15:20

for a, b being Real
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 )