let n be Nat; :: thesis: 0_No <= uInt . n
( 0 = n or 0 < n ) ;
then ( uInt . 0 = uInt . n or uInt . 0 < uInt . n ) by Th3;
hence 0_No <= uInt . n by Def1; :: thesis: verum