let i, j be Integer; :: thesis: ( i < j implies uInt . i < uInt . j )
assume A1: i < j ; :: thesis: uInt . i < uInt . j
i in INT by INT_1:def 2;
then consider k being Nat such that
A2: ( i = k or i = - k ) by INT_1:def 1;
j in INT by INT_1:def 2;
then consider n being Nat such that
A3: ( j = n or j = - n ) by INT_1:def 1;

per cases ( k < n or k > n or k = n ) by XXREAL_0:1;

suppose k < n ; :: thesis: uInt . i < uInt . j

then ( - n < k & - n < - k & - k < n ) by XREAL_1:24;
hence uInt . i < uInt . j by A2, A3, A1, Lm3; :: thesis: verum

end;

suppose k > n ; :: thesis: uInt . i < uInt . j

hence uInt . i < uInt . j by Lm3, A2, A3, A1; :: thesis: verum

end;

suppose k = n ; :: thesis: uInt . i < uInt . j

then ( i = - n & j = n & - n < 0 & 0 < n ) by A2, A3, A1;
then ( uInt . i < uInt . 0 & uInt . 0 <= uInt . j ) by Lm3;
hence uInt . i < uInt . j by SURREALO:4; :: thesis: verum

end;

end;