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 object ; :: 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 Nat : j < n + 1 } by AXIOMS:4;
then consider j being 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;

A3: Segm 1 c= Segm (n + 1) by NAT_1:39, NAT_1:11;
Seg n c= Segm (n + 1) by Th2;
hence {0} \/ (Seg n) c= n + 1 by A3, CARD_1:49, XBOOLE_1:8; :: thesis: verum