let m, n be natural Number ; :: thesis: ( not m < n + 1 or m < n or m = n )
assume m < n + 1 ; :: thesis: ( m < n or m = n )
then m <= n by Th13;
hence ( m < n or m = n ) by XXREAL_0:1; :: thesis: verum