let a be natural Number ; :: thesis: ( a = 0 or a in Seg a )
assume a <> 0 ; :: thesis: a in Seg a
then ex b being Nat st a = b + 1 by NAT_1:6;
then ( a in NAT & 1 <= a ) by NAT_1:11;
hence a in Seg a ; :: thesis: verum