Written by Ayal, slight modifications by Avital.
Theorem: If and then Proof
Let's assume that a > b and try to reach a contradiction.
Now let's choose epsilon = (a - b)/4 - so according to the lim def, we reach two conclusions:
1. There exists an m1 such that for any n > m1: |a_n - a| < (a - b)/4
and
2. There exists an m2 such that for any n > m2: |a_n - b| < (a - b)/4
Define n = max(m1,m2)+1. n > m1, hence: |a_n - a| < (a - b)/4 and n > m2, hence: |a_n - b| < (a - b)/4 ---> (a - (a - b)/4 < a_n < a + (a - b)/4) and (b - (a - b)/4 < a_n < b + (a - b)/4) --->*---> false.
Q.E.D.