let n be 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:4;
then consider j being Element of NAT such that
A1: j = x and
A2: j < n + 1 ;
( j = 0 or ( 1 < j + 1 & j <= n ) ) by A2, NAT_1:13, XREAL_1:29;
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:1, 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 A3: {0} c= n + 1 by CARD_1:49, NAT_1:39;
Seg n c= n + 1 by Th5;
hence {0} \/ (Seg n) c= n + 1 by A3, XBOOLE_1:8; :: thesis: verum