let N be ExtNat; :: thesis: ( N = 0 or ex K being ExtNat st N = K + 1 )

per cases ( N is Nat or N = +infty ) by Th3;

suppose N is Nat ; :: thesis: ( N = 0 or ex K being ExtNat st N = K + 1 )

then reconsider n = N as Nat ;
assume N <> 0 ; :: thesis: ex K being ExtNat st N = K + 1
then consider k being Nat such that
A1: n = k + 1 by NAT_1:6;
reconsider K = k as ExtNat ;
take K ; :: thesis: N = K + 1
N = k + 1 by A1;
hence N = K + 1 ; :: thesis: verum

end;

suppose A2: N = +infty ; :: thesis: ( N = 0 or ex K being ExtNat st N = K + 1 )

assume N <> 0 ; :: thesis: ex K being ExtNat st N = K + 1
take +infty ; :: thesis: N = +infty + 1
thus N = +infty + 1 by A2, XXREAL_3:def 2; :: thesis: verum

end;

end;