let b, a be natural number ; :: thesis: ( b = 0 or b + a in seq a,b )
assume b <> 0 ; :: thesis: b + a in seq a,b
then consider c being Nat such that
A1: b = c + 1 by NAT_1:6;
A2: b + a is Element of NAT by ORDINAL1:def 13;
1 <= b by A1, NAT_1:11;
then ( 1 + a <= b + a & b + a <= b + a ) by XREAL_1:8;
hence b + a in seq a,b by A2; :: thesis: verum