let i, j be Integer; :: thesis: ( i < j iff uInt . i < uInt . j )
thus ( i < j implies uInt . i < uInt . j ) by Lm4; :: thesis: ( uInt . i < uInt . j implies i < j )
assume A1: ( uInt . i < uInt . j & j <= i ) ; :: thesis: contradiction
then j <> i by SURREALO:3;
then j < i by A1, XXREAL_0:1;
then uInt . j <= uInt . i by Lm4;
hence contradiction by A1; :: thesis: verum