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;