let i, j be Nat; :: thesis: ( not i <= j or i = j or i + 1 <= j )
assume i <= j ; :: thesis: ( i = j or i + 1 <= j )
then i + 1 <= j + 1 by XREAL_1:6;
hence ( i = j or i + 1 <= j ) by NAT_1:8, XCMPLX_1:2; :: thesis: verum