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;