let N, M be ExtNat; :: thesis: ( not N <= M + 1 or N <= M or N = M + 1 )
assume A1: N <= M + 1 ; :: thesis: ( N <= M or N = M + 1 )
per cases ( M is Nat or M = +infty ) by Th3;
suppose M is Nat ; :: thesis: ( N <= M or N = M + 1 )
then reconsider m = M as Nat ;
m + 1 = M + 1 ;
then A2: ( m + 1 in NAT & N <= m + 1 ) by A1;
then N in NAT by Th5;
then reconsider n = N as Nat ;
( n <= m or n = m + 1 ) by A2, NAT_1:8;
then ( N <= M or N = m + 1 ) ;
hence ( N <= M or N = M + 1 ) ; :: thesis: verum
end;
suppose M = +infty ; :: thesis: ( N <= M or N = M + 1 )
hence ( N <= M or N = M + 1 ) by A1, XXREAL_3:def 2; :: thesis: verum
end;
end;