let n be Nat; :: thesis: uInt . (- (n + 1)) < uInt . (- n)
A1: uInt . (- (n + 1)) = [{},{(uInt . (- n))}] by Def1;
assume uInt . (- n) <= uInt . (- (n + 1)) ; :: thesis: contradiction
then {(uInt . (- n))} << R_ (uInt . (- (n + 1))) by SURREAL0:43;
then ( uInt . (- n) in {(uInt . (- n))} & {(uInt . (- n))} << {(uInt . (- n))} ) by A1, TARSKI:def 1;
hence contradiction by SURREALO:3; :: thesis: verum