let n be Element of NAT ; :: thesis: n + 1 = {0 } \/ (Seg n)
thus n + 1 c= {0 } \/ (Seg n) :: according to XBOOLE_0:def 10 :: thesis: {0 } \/ (Seg n) c= n + 1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in n + 1 or x in {0 } \/ (Seg n) )
assume x in n + 1 ; :: thesis: x in {0 } \/ (Seg n)
then x in { j where j is Element of NAT : j < n + 1 } by AXIOMS:30;
then consider j being Element of NAT such that
A1: ( j = x & j < n + 1 ) ;
( j = 0 or ( 0 < j & j <= n ) ) by A1, NAT_1:13;
then ( j = 0 or ( 1 < j + 1 & j <= n ) ) by XREAL_1:31;
then ( j = 0 or ( 1 <= j & j <= n ) ) by NAT_1:13;
then ( x in {0 } or x in Seg n ) by A1, FINSEQ_1:3, TARSKI:def 1;
hence x in {0 } \/ (Seg n) by XBOOLE_0:def 3; :: thesis: verum

end;

1 <= n + 1 by NAT_1:11;
then A2: {0 } c= n + 1 by CARD_1:87, NAT_1:40;
Seg n c= n + 1 by Th5;
hence {0 } \/ (Seg n) c= n + 1 by A2, XBOOLE_1:8; :: thesis: verum