let a, b be Integer; :: thesis: for n being Nat st a <= b & b <= a + n holds
not not b = a + 0 & ... & not b = a + n
let n be Nat; :: thesis: ( a <= b & b <= a + n implies not not b = a + 0 & ... & not b = a + n )
assume ( a <= b & b <= a + n ) ; :: thesis: not not b = a + 0 & ... & not b = a + n
then A2: ( a - a <= b - a & b - a <= (a + n) - a ) by XREAL_1:9;
then reconsider k = b - a as Nat ;
b = a + k ;
hence not not b = a + 0 & ... & not b = a + n by A2; :: thesis: verum