let n be Nat; :: thesis: uInt . n < uInt . (n + 1)
A1: uInt . (n + 1) = [{(uInt . n)},{}] by Def1;
assume uInt . (n + 1) <= uInt . n ; :: thesis: contradiction
then L_ (uInt . (n + 1)) << {(uInt . n)} 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